1 /-
2 Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Sébastien Gouëzel, Yury Kudryashov
5 -/
6
7 import analysis.calculus.local_extr
src └──────────────────────────┘
8 import analysis.convex.topology
src └──────────────────────┘
9
10 /-!
11 # The mean value inequality and equalities
12
13 In this file we prove the following facts:
14
15 * `convex.norm_image_sub_le_of_norm_deriv_le` : if `f` is differentaible on a convex set `s`
16 and the norm of its derivative is bounded by `C`, then `f` is Lipschitz continuous on `s` with
17 constant `C`.
18
19 * `image_le_of*`, `image_norm_le_of_*` : several similar lemmas deducing `f x ≤ B x` or
20 `∥f x∥ ≤ B x` from upper estimates on `f'` or `∥f'∥`, respectively. These lemmas differ by
21 their assumptions:
22
23 * `of_liminf_*` lemmas assume that limit inferior of some ratio is less than `B' x`;
24 * `of_deriv_right_*`, `of_norm_deriv_right_*` lemmas assume that the right derivative
25 or its norm is less than `B' x`;
26 * `of_*_lt_*` lemmas assume a strict inequality whenever `f x = B x` or `∥f x∥ = B x`;
27 * `of_*_le_*` lemmas assume a non-strict inequality everywhere on `[a, b)`;
28 * name of a lemma ends with `'` if (1) it assumes that `B` is continuous on `[a, b]`
29 and has a right derivative at every point of `[a, b)`, and (2) the lemma has
30 a counterpart assuming that `B` is differentiable everywhere on `ℝ`
31
32 * `norm_image_sub_le_*_segment` : if derivative of `f` on `[a, b]` is bounded above
33 by a constant `C`, then `∥f x - f a∥ ≤ C * ∥x - a∥`; several versions deal with
34 right derivative and derivative within `[a, b]` (`has_deriv_within_at` or `deriv_within`).
35
36 * `convex.is_const_of_fderiv_within_eq_zero` : if a function has derivative `0` on a convex set `s`,
37 then it is a constant on `s`.
38
39 * `exists_ratio_has_deriv_at_eq_ratio_slope` and `exists_ratio_deriv_eq_ratio_slope` :
40 Cauchy's Mean Value Theorem.
41
42 * `exists_has_deriv_at_eq_slope` and `exists_deriv_eq_slope` : Lagrange's Mean Value Theorem.
43
44 * `convex.image_sub_lt_mul_sub_of_deriv_lt`, `convex.mul_sub_lt_image_sub_of_lt_deriv`,
45 `convex.image_sub_le_mul_sub_of_deriv_le`, `convex.mul_sub_le_image_sub_of_le_deriv`,
46 if `∀ x, C (</≤/>/≥) (f' x)`, then `C * (y - x) (</≤/>/≥) (f y - f x)` whenever `x < y`.
47
48 * `convex.mono_of_deriv_nonneg`, `convex.antimono_of_deriv_nonpos`,
49 `convex.strict_mono_of_deriv_pos`, `convex.strict_antimono_of_deriv_neg` :
50 if the derivative of a function is non-negative/non-positive/positive/negative, then
51 the function is monotone/monotonically decreasing/strictly monotone/strictly monotonically
52 decreasing.
53
54 * `convex_on_of_deriv_mono`, `convex_on_of_deriv2_nonneg` : if the derivative of a function
55 is increasing or its second derivative is nonnegative, then the original function is convex.
56 -/
57
58 set_option class.instance_max_depth 120
doc └──────────────────────┘
59
60 variables {E : Type*} [normed_group E] [normed_space ℝ E]
id └──────────┘ └──────────┘ ┴
src └──────────┘ └──────────┘ ┴
typ └──────────┘ └──────────┘ ┴
doc └──────────┘ └──────────┘
61 {F : Type*} [normed_group F] [normed_space ℝ F]
id └──────────┘ └──────────┘ ┴
src └──────────┘ └──────────┘ ┴
typ └──────────┘ └──────────┘ ┴
doc └──────────┘ └──────────┘
62
63 open metric set lattice asymptotics continuous_linear_map filter
64 open_locale classical topological_space
65
66 /-! ### One-dimensional fencing inequalities -/
67
68 /-- General fencing theorem for continuous functions with an estimate on the derivative.
69 Let `f` and `B` be continuous functions on `[a, b]` such that
70
71 * `f a ≤ B a`;
72 * `B` has right derivative `B'` at every point of `[a, b)`;
73 * for each `x ∈ [a, b)` the right-side limit inferior of `(f z - f x) / (z - x)`
74 is bounded above by a function `f'`;
75 * we have `f' x < B' x` whenever `f x = B x`.
76
77 Then `f x ≤ B x` everywhere on `[a, b]`. -/
78 lemma image_le_of_liminf_slope_right_lt_deriv_boundary' {f f' : ℝ → ℝ} {a b : ℝ}
id ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴
79 (hf : continuous_on f (Icc a b))
id └───────────┘ ┴ └─┘ ┴ ┴
src └───────────┘ └─┘
typ └───────────┘ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
80 -- `hf'` actually says `liminf (z - x)⁻¹ * (f z - f x) ≤ f' x`
81 (hf' : ∀ x ∈ Ico a b, ∀ r, f' x < r →
id ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
doc └─┘
82 ∃ᶠ z in nhds_within x (Ioi x), (z - x)⁻¹ * (f z - f x) < r)
id └┘ ┴ └┘ └─────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ └┘ └─────────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴
typ └┘ ┴ └┘ └─────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └┘ └─────────┘ └─┘ ┴
83 {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : continuous_on B (Icc a b))
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ └─┘ ┴ ┴
src ┴ ┴ ┴ └───────────┘ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
84 (hB' : ∀ x ∈ Ico a b, has_deriv_within_at B (B' x) (Ioi x) x)
id ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
src └─┘ └─────────────────┘ └─┘
typ ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
doc └─┘ └─────────────────┘ └─┘
85 (bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x) :
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └─┘ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └─┘
86 ∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x :=
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
87 begin
st └─────
88 change Icc a b ⊆ {x | f x ≤ B x},
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘└─┘┴ ┴ ┴┴┴┴└──┘ ┴ ┴ ┴ ┴ ┴
typ └─────┘└─┘┴┴┴┴┴┴┴┴└──┘┴┴ ┴ ┴┴┴ ┴
doc └─────┘└─┘┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────┘└─
89 set s := {x | f x ≤ B x} ∩ Icc a b,
id ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src └───────┘ └──┘ ┴ ┴┴┴ ┴ └┘┴┴└─┘┴ ┴
typ └───────┘ └──┘┴┴ ┴┴┴┴┴ └┘┴┴└─┘┴┴┴┴
doc └───────┘ └──┘ ┴ ┴ ┴ ┴ └┘ ┴└─┘┴ ┴
txt └───────┘ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par └───────┘ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid ┴┴┴└┘┴ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ───────────────────────────────────┘└─
90 have A : continuous_on (λ x, (f x, B x)) (Icc a b), from hf.prod hB,
id └───────────┘ ┴┴ ┴ └─┘ ┴ ┴ └─────┘ └┘
src └───────┘└───────────┘┴ └──┘┴ ┴ └┘ ┴ └─┘ └─┘┴ ┴ ┴ └───┘└─────┘┴
typ └───────┘└───────────┘┴ └──┘┴┴┴ └┘┴┴ └─┘ └─┘┴┴┴┴┴ └───┘└─────┘┴└┘
doc └───────┘└───────────┘┴ └──┘ ┴ └┘ ┴ └─┘ └─┘┴ ┴ ┴ └───┘ ┴
txt └───────┘ ┴ └──┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └───┘ ┴
par └───────┘ ┴ └──┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └───┘ ┴
pid └────┘└─┘ ┴ └──┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └───┘ ┴
st ───────────────────────────────────────────────────┘└───────────────┘└─
91 have : is_closed s,
id └───────┘ ┴
src └─────┘└───────┘┴
typ └─────┘└───────┘┴┴
doc └─────┘└───────┘┴
txt └─────┘ ┴
par └─────┘ ┴
pid └───┘└┘ ┴
st ───────────────────┘└─
92 { simp only [s, inter_comm],
id ┴ └────────┘
src └─────────┘ └┘└────────┘┴
typ └─────────┘┴└┘└────────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ───┘└───────────────────────┘└─
93 exact A.preimage_closed_of_closed is_closed_Icc (order_closed_topology.is_closed_le' _) },
id └─────────────────────────┘ └───────────┘ └─────────────────────────────────┘
src └────┘└─────────────────────────┘┴└───────────┘┴ └─────────────────────────────────┘└──┘
typ └────┘└─────────────────────────┘┴└───────────┘┴ └─────────────────────────────────┘└──┘
doc └────┘ ┴ ┴ └──┘
txt └────┘ ┴ ┴ └──┘
par └────┘ ┴ ┴ └──┘
pid ┴ ┴ ┴ └─┘┴
st ───────────────────────────────────────────────────────────────────────────────────────────┘└┘└
94 apply this.Icc_subset_of_forall_exists_gt ha,
id └─────────────────────────────────┘ └┘
src └────┘└─────────────────────────────────┘┴
typ └────┘└─────────────────────────────────┘┴└┘
doc └────┘└─────────────────────────────────┘┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────────────────────────────┘└─
95 rintros x ⟨hxB, xab⟩ y hy,
src └───────────────────────┘
typ └───────────────────────┘
doc └───────────────────────┘
txt └───────────────────────┘
par └───────────────────────┘
pid └────────────────┘
st ──────────────────────────┘└─
96 change f x ≤ B x at hxB,
id ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴ ┴ └─────┘
typ └─────┘┴┴ ┴ ┴┴┴┴└─────┘
doc └─────┘ ┴ ┴ ┴ ┴ └─────┘
txt └─────┘ ┴ ┴ ┴ ┴ └─────┘
par └─────┘ ┴ ┴ ┴ ┴ └─────┘
pid ┴ ┴ ┴ ┴ ┴ ┴└────┘
st ────────────────────────┘└─
97 cases lt_or_eq_of_le hxB with hxB hxB,
id └────────────┘ └─┘
src └────┘└────────────┘┴ └───────────┘
typ └────┘└────────────┘┴└─┘└───────────┘
doc └────┘ ┴ └───────────┘
txt └────┘ ┴ └───────────┘
par └────┘ ┴ └───────────┘
pid ┴ ┴ └───────────┘
st ──────────────────────────────────────┘└─
98 { -- If `f x < B x`, then all we need is continuity of both sides
st ───┘└───────────────────────────────────────────────────────────────
99 apply nonempty_of_mem_sets (nhds_within_Ioi_self_ne_bot x),
id └──────────────────┘ └─────────────────────────┘ ┴
src └────┘└──────────────────┘┴ └─────────────────────────┘┴ ┴
typ └────┘└──────────────────┘┴ └─────────────────────────┘┴┴┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────┘└─
100 refine inter_mem_sets _ (Ioc_mem_nhds_within_Ioi ⟨le_refl x, hy⟩),
id └────────────┘ └─────────────────────┘ └─────┘ ┴ └┘
src └─────┘└────────────┘└─┘ └─────────────────────┘┴ └─────┘┴ └┘ └┘
typ └─────┘└────────────┘└─┘ └─────────────────────┘┴ └─────┘┴┴└┘└┘└┘
doc └─────┘ └─┘ ┴ ┴ └┘ └┘
txt └─────┘ └─┘ ┴ ┴ └┘ └┘
par └─────┘ └─┘ ┴ ┴ └┘ └┘
pid ┴ └─┘ ┴ ┴ └┘ └┘
st ────────────────────────────────────────────────────────────────────┘└─
101 have : ∀ᶠ x in nhds_within x (Icc a b), f x < B x,
id └┘ └┘ └─────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘└┘└─┘└┘┴└─────────┘┴ ┴ └─┘┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴
typ └─────┘└┘└─┘└┘┴└─────────┘┴┴┴ └─┘┴┴┴┴┴┴┴┴┴ ┴┴┴┴┴
doc └─────┘└┘└─┘└┘┴└─────────┘┴ ┴ └─┘┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴
txt └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────┘└─
102 from A x (Ico_subset_Icc_self xab)
id ┴ ┴ └─────────────────┘ └─┘
src └───┘ ┴ ┴ └─────────────────┘┴ └─
typ └───┘┴┴┴┴ └─────────────────┘┴└─┘└─
doc └───┘ ┴ ┴ ┴ └─
txt └───┘ ┴ ┴ ┴ └─
par └───┘ ┴ ┴ ┴ └─
pid └───┘ ┴ ┴ ┴ └─
st ─────────────────────────────────────────
103 (mem_nhds_sets (is_open_lt continuous_fst continuous_snd) hxB),
id └───────────┘ └────────┘ └────────────┘ └────────────┘ └─┘
src ───────┘ └───────────┘┴ └────────┘┴└────────────┘┴└────────────┘└┘ ┴
typ ───────┘ └───────────┘┴ └────────┘┴└────────────┘┴└────────────┘└┘└─┘┴
doc ───────┘ ┴ ┴ ┴ └┘ ┴
txt ───────┘ ┴ ┴ ┴ └┘ ┴
par ───────┘ ┴ ┴ ┴ └┘ ┴
pid ───────┘ ┴ ┴ ┴ └┘ ┴
st ─────────────────────────────────────────────────────────────────────┘└─
104 have : ∀ᶠ x in nhds_within x (Ioi x), f x < B x,
id └┘ └┘ └─────────┘ └─┘ ┴ ┴ ┴ ┴
src └─────┘└┘└─┘└┘┴└─────────┘┴ ┴ └─┘┴ ┴┴┴ ┴ ┴ ┴ ┴
typ └─────┘└┘└─┘└┘┴└─────────┘┴ ┴ └─┘┴┴┴┴┴┴┴ ┴ ┴┴┴
doc └─────┘└┘└─┘└┘┴└─────────┘┴ ┴ └─┘┴ ┴┴┴ ┴ ┴ ┴ ┴
txt └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────┘┴└─────────────────┘└─
105 from nhds_within_le_of_mem (Icc_mem_nhds_within_Ioi xab) this,
id └───────────────────┘ └─────────────────────┘ └─┘ └──┘
src └───┘└───────────────────┘┴ └─────────────────────┘┴ └┘
typ └───┘└───────────────────┘┴ └─────────────────────┘┴└─┘└┘└──┘
doc └───┘ ┴ ┴ └┘
txt └───┘ ┴ ┴ └┘
par └───┘ ┴ ┴ └┘
pid └───┘ ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────────┘└─
106 refine mem_sets_of_superset this (set_of_subset_set_of.2 $ λ y, le_of_lt) },
id └──────────────────┘ └──┘ └──────────────────┘ └──────┘
src └─────┘└──────────────────┘┴ ┴ └──────────────────┘└─┘ ┴ └──┘└──────┘└┘
typ └─────┘└──────────────────┘┴└──┘┴ └──────────────────┘└─┘ ┴ └──┘└──────┘└┘
doc └─────┘ ┴ ┴ └─┘ ┴ └──┘ └┘
txt └─────┘ ┴ ┴ └─┘ ┴ └──┘ └┘
par └─────┘ ┴ ┴ └─┘ ┴ └──┘ └┘
pid ┴ ┴ ┴ └─┘ ┴ └──┘ ┴┴
st ─────────────────────────────────────────────────────────────────────────────┘└┘└
107 { rcases dense (bound x xab hxB) with ⟨r, hfr, hrB⟩,
id └───┘ └───┘ ┴ └─┘ └─┘
src └─────┘└───┘┴ ┴ ┴ ┴ └──────────────────┘
typ └─────┘└───┘┴ └───┘┴┴┴└─┘┴└─┘└──────────────────┘
doc └─────┘ ┴ ┴ ┴ ┴ └──────────────────┘
txt └─────┘ ┴ ┴ ┴ ┴ └──────────────────┘
par └─────┘ ┴ ┴ ┴ ┴ └──────────────────┘
pid ┴ ┴ ┴ ┴ ┴ └──────────────────┘
st ────────────────────────────────────────────────────┘└─
108 specialize hf' x xab r hfr,
id └─┘ ┴ └─┘ ┴ └─┘
src └─────────┘ ┴ ┴ ┴ ┴
typ └─────────┘└─┘┴┴┴└─┘┴┴┴└─┘
doc └─────────┘ ┴ ┴ ┴ ┴
txt └─────────┘ ┴ ┴ ┴ ┴
par └─────────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────┘└─
109 have HB : ∀ᶠ z in nhds_within x (Ioi x), r < (z - x)⁻¹ * (B z - B x),
id └┘ └┘ └─────────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
src └────────┘└┘└─┘└┘┴└─────────┘┴ ┴ └─┘┴ ┴┴┴ ┴ ┴ ┴┴┴ ┴└┘┴┴┴ ┴ ┴ ┴ ┴ ┴
typ └────────┘└┘└─┘└┘┴└─────────┘┴ ┴ └─┘┴┴┴┴┴┴┴ ┴ ┴┴┴ ┴└┘┴┴┴ ┴ ┴ ┴┴┴ ┴
doc └────────┘└┘└─┘└┘┴└─────────┘┴ ┴ └─┘┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └─────┘└─┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────┘└─
110 from (has_deriv_within_at_iff_tendsto_slope' $ lt_irrefl x).1 (hB' x xab)
id └────────────────────────────────────┘ └───────┘ └─┘ ┴ └─┘
src └───┘ └────────────────────────────────────┘┴ ┴└───────┘┴ └──┘ ┴ ┴ └─
typ └───┘ └────────────────────────────────────┘┴ ┴└───────┘┴ └──┘ └─┘┴┴┴└─┘└─
doc └───┘ ┴ ┴ ┴ └──┘ ┴ ┴ └─
txt └───┘ ┴ ┴ ┴ └──┘ ┴ ┴ └─
par └───┘ ┴ ┴ ┴ └──┘ ┴ ┴ └─
pid └───┘ ┴ ┴ ┴ └──┘ ┴ ┴ └─
st ────────────────────────────────────────────────────────────────────────────────
111 (mem_nhds_sets is_open_Ioi hrB),
id └───────────┘ └─────────┘ └─┘
src ───────┘ └───────────┘┴└─────────┘┴ ┴
typ ───────┘ └───────────┘┴└─────────┘┴└─┘┴
doc ───────┘ ┴ ┴ ┴
txt ───────┘ ┴ ┴ ┴
par ───────┘ ┴ ┴ ┴
pid ───────┘ ┴ ┴ ┴
st ──────────────────────────────────────┘└─
112 obtain ⟨z, ⟨hfz, hzB⟩, hz⟩ :
src └────────────────────────────
typ └────────────────────────────
doc └────────────────────────────
txt └────────────────────────────
par └────────────────────────────
pid └──────────────────────
st ─────────────────────────────────
113 ∃ z, ((z - x)⁻¹ * (f z - f x) < r ∧ r < (z - x)⁻¹ * (B z - B x)) ∧ z ∈ Ioc x y,
id ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src ─────┘┴└┘┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴┴┴└─┘┴ ┴
typ ─────┘┴└┘┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ └┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ └─┘ ┴ ┴┴┴└─┘┴┴┴┴
doc ─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴└─┘┴ ┴
txt ─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
par ─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
pid ─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────────────┘└─
114 from ((hf'.and_eventually HB).and_eventually
id └────────────────┘ └┘
src └───┘ └────────────────┘┴ └────────────────
typ └───┘ └────────────────┘┴└┘└────────────────
doc └───┘ ┴ └────────────────
txt └───┘ ┴ └────────────────
par └───┘ ┴ └────────────────
pid └───┘ ┴ └────────────────
st ───────────────────────────────────────────────────
115 (Ioc_mem_nhds_within_Ioi ⟨le_refl _, hy⟩)).exists,
id └─────────────────────┘ └─────┘ └┘
src ───────┘ └─────────────────────┘┴ └─────┘└──┘ └────────┘
typ ───────┘ └─────────────────────┘┴ └─────┘└──┘└┘└────────┘
doc ───────┘ ┴ └──┘ └────────┘
txt ───────┘ ┴ └──┘ └────────┘
par ───────┘ ┴ └──┘ └────────┘
pid ───────┘ ┴ └──┘ └───────┘┴
st ────────────────────────────────────────────────────────┘└─
116 have := le_of_lt (lt_trans hfz hzB),
id └──────┘ └──────┘ └─┘ └─┘
src └──────┘└──────┘┴ └──────┘┴ ┴ ┴
typ └──────┘└──────┘┴ └──────┘┴└─┘┴└─┘┴
doc └──────┘ ┴ ┴ ┴ ┴
txt └──────┘ ┴ ┴ ┴ ┴
par └──────┘ ┴ ┴ ┴ ┴
pid └───┘└─┘ ┴ ┴ ┴ ┴
st ──────────────────────────────────────┘└─
117 refine ⟨z, _, hz⟩,
id ┴ └┘
src └─────┘ └───┘ ┴
typ └─────┘ ┴└───┘└┘┴
doc └─────┘ └───┘ ┴
txt └─────┘ └───┘ ┴
par └─────┘ └───┘ ┴
pid ┴ └───┘ ┴
st ────────────────────┘└─
118 rw [mul_le_mul_left (inv_pos $ sub_pos.2 hz.1), hxB, sub_le_sub_iff_right] at this,
id └─────────────┘ └─────┘ └─────┘ └┘ └─┘ └──────────────────┘
src └──┘└─────────────┘┴ └─────┘┴ ┴└─────┘└─┘ └───┘ └┘└──────────────────┘└───────┘
typ └──┘└─────────────┘┴ └─────┘┴ ┴└─────┘└─┘└┘└───┘└─┘└┘└──────────────────┘└───────┘
doc └──┘ ┴ ┴ ┴ └─┘ └───┘ └┘ └───────┘
txt └──┘ ┴ ┴ ┴ └─┘ └───┘ └┘ └───────┘
par └──┘ ┴ ┴ ┴ └─┘ └───┘ └┘ └───────┘
pid └┘ ┴ ┴ ┴ └─┘ └───┘ └┘ ┴└──────┘
st ─────────────────────────────────────────────────┘└───┘└────────────────────┘┴└──────┘└─
119 exact this }
id └──┘
src └────┘ ┴
typ └────┘└──┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────┘└─
120 end
st ──┘
121
122 /-- General fencing theorem for continuous functions with an estimate on the derivative.
123 Let `f` and `B` be continuous functions on `[a, b]` such that
124
125 * `f a ≤ B a`;
126 * `B` has derivative `B'` everywhere on `ℝ`;
127 * for each `x ∈ [a, b)` the right-side limit inferior of `(f z - f x) / (z - x)`
128 is bounded above by a function `f'`;
129 * we have `f' x < B' x` whenever `f x = B x`.
130
131 Then `f x ≤ B x` everywhere on `[a, b]`. -/
132 lemma image_le_of_liminf_slope_right_lt_deriv_boundary {f f' : ℝ → ℝ} {a b : ℝ}
id ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴
133 (hf : continuous_on f (Icc a b))
id └───────────┘ ┴ └─┘ ┴ ┴
src └───────────┘ └─┘
typ └───────────┘ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
134 -- `hf'` actually says `liminf (z - x)⁻¹ * (f z - f x) ≤ f' x`
135 (hf' : ∀ x ∈ Ico a b, ∀ r, f' x < r →
id ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
doc └─┘
136 ∃ᶠ z in nhds_within x (Ioi x), (z - x)⁻¹ * (f z - f x) < r)
id └┘ ┴ └┘ └─────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ └┘ └─────────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴
typ └┘ ┴ └┘ └─────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └┘ └─────────┘ └─┘ ┴
137 {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : ∀ x, has_deriv_at B (B' x) x)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ └┘ ┴ ┴
src ┴ ┴ ┴ └──────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ └┘ ┴ ┴
doc └──────────┘
138 (bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x) :
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └─┘ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └─┘
139 ∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x :=
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
140 image_le_of_liminf_slope_right_lt_deriv_boundary' hf hf' ha
id └───────────────────────────────────────────────┘ └┘ └─┘ └┘
src └───────────────────────────────────────────────┘
typ └───────────────────────────────────────────────┘ └┘ └─┘ └┘
doc └───────────────────────────────────────────────┘
141 (λ x hx, (hB x).continuous_at.continuous_within_at)
id ┴ └┘ └┘ ┴ └───────────┘ └──────────────────┘
src └───────────┘ └──────────────────┘
typ ┴ └┘ └┘ ┴ └───────────┘ └──────────────────┘
142 (λ x hx, (hB x).has_deriv_within_at) bound
id ┴ └┘ └┘ ┴ └─────────────────┘ └───┘
src └─────────────────┘
typ ┴ └┘ └┘ ┴ └─────────────────┘ └───┘
143
144 /-- General fencing theorem for continuous functions with an estimate on the derivative.
145 Let `f` and `B` be continuous functions on `[a, b]` such that
146
147 * `f a ≤ B a`;
148 * `B` has right derivative `B'` at every point of `[a, b)`;
149 * for each `x ∈ [a, b)` the right-side limit inferior of `(f z - f x) / (z - x)`
150 is bounded above by `B'`.
151
152 Then `f x ≤ B x` everywhere on `[a, b]`. -/
153 lemma image_le_of_liminf_slope_right_le_deriv_boundary {f : ℝ → ℝ} {a b : ℝ}
id ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴
154 (hf : continuous_on f (Icc a b))
id └───────────┘ ┴ └─┘ ┴ ┴
src └───────────┘ └─┘
typ └───────────┘ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
155 {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : continuous_on B (Icc a b))
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ └─┘ ┴ ┴
src ┴ ┴ ┴ └───────────┘ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
156 (hB' : ∀ x ∈ Ico a b, has_deriv_within_at B (B' x) (Ioi x) x)
id ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
src └─┘ └─────────────────┘ └─┘
typ ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
doc └─┘ └─────────────────┘ └─┘
157 -- `bound` actually says `liminf (z - x)⁻¹ * (f z - f x) ≤ B' x`
158 (bound : ∀ x ∈ Ico a b, ∀ r, B' x < r →
id ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
doc └─┘
159 ∃ᶠ z in nhds_within x (Ioi x), (z - x)⁻¹ * (f z - f x) < r) :
id └┘ ┴ └┘ └─────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ └┘ └─────────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴
typ └┘ ┴ └┘ └─────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └┘ └─────────┘ └─┘ ┴
160 ∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x :=
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
161 begin
st └─────
162 have Hr : ∀ x ∈ Icc a b, ∀ r ∈ Ioi (0:ℝ), f x ≤ B x + r * (x - a),
id └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └───┘└─┘┴ ┴ ┴ └───┘└─┘┴ └┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴┴┴ ┴┴┴ ┴
typ └────────┘ └───┘└─┘┴ ┴┴ ┴ └───┘└─┘┴ └┘ ┴ ┴┴┴ ┴┴┴┴┴ ┴┴┴ ┴┴┴ ┴┴┴┴┴
doc └────────┘ └───┘└─┘┴ ┴ ┴ └───┘└─┘┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └────────┘ └───┘ ┴ ┴ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └────────┘ └───┘ ┴ ┴ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └─────┘└─┘ └───┘ ┴ ┴ ┴ └───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────┘└─
163 { intros x hx r hr,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ───┘└──────────────┘└─
164 apply image_le_of_liminf_slope_right_lt_deriv_boundary' hf bound,
id └───────────────────────────────────────────────┘ └┘ └───┘
src └────┘└───────────────────────────────────────────────┘┴ ┴
typ └────┘└───────────────────────────────────────────────┘┴└┘┴└───┘
doc └────┘└───────────────────────────────────────────────┘┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────┘└─
165 { rwa [sub_self, mul_zero, add_zero] },
id └──────┘ └──────┘ └──────┘
src └───┘└──────┘└┘└──────┘└┘└──────┘└┘
typ └───┘└──────┘└┘└──────┘└┘└──────┘└┘
doc └───┘ └┘ └┘ └┘
txt └───┘ └┘ └┘ └┘
par └───┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st ─────┘└───────────┘└────────┘└────────┘┴┴└┘└
166 { exact hB.add (continuous_on_const.mul
id └────┘ └─────────────────────┘
src └────┘└────┘┴ └─────────────────────┘└
typ └────┘└────┘┴ └─────────────────────┘└
doc └────┘ ┴ └
txt └────┘ ┴ └
par └────┘ ┴ └
pid ┴ ┴ └
st ─────┘└─────────────────────────────────────
167 (continuous_id.continuous_on.sub continuous_on_const)) },
id └─────────────────────────────┘ └─────────────────┘
src ───────┘ └─────────────────────────────┘┴└─────────────────┘└─┘
typ ───────┘ └─────────────────────────────┘┴└─────────────────┘└─┘
doc ───────┘ ┴ └─┘
txt ───────┘ ┴ └─┘
par ───────┘ ┴ └─┘
pid ───────┘ ┴ └┘┴
st ──────────────────────────────────────────────────────────────┘└┘└
168 { assume x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ─────┘└─────────┘└─
169 exact (hB' x hx).add (((has_deriv_within_at_id x (Ioi x)).sub_const a).const_mul r) },
id └─┘ └┘ └────────────────────┘ └─┘ ┴ ┴ ┴
src └────┘ ┴ ┴ └────┘ └────────────────────┘┴ ┴ └─┘┴ └───────────┘ └──────────┘ └┘
typ └────┘ └─┘┴ ┴└┘└────┘ └────────────────────┘┴ ┴ └─┘┴┴└───────────┘┴└──────────┘┴└┘
doc └────┘ ┴ ┴ └────┘ ┴ ┴ └─┘┴ └───────────┘ └──────────┘ └┘
txt └────┘ ┴ ┴ └────┘ ┴ ┴ ┴ └───────────┘ └──────────┘ └┘
par └────┘ ┴ ┴ └────┘ ┴ ┴ ┴ └───────────┘ └──────────┘ └┘
pid ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └───────────┘ └──────────┘ ┴┴
st ─────────────────────────────────────────────────────────────────────────────────────────┘└┘└
170 { assume x hx _,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └───────────┘
st ─────┘└───────────┘└─
171 rw [mul_one],
id └─────┘
src └──┘└─────┘┴
typ └──┘└─────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ────────────────┘└──
172 exact (lt_add_iff_pos_right _).2 hr },
id └──────────────────┘ └┘
src └────┘ └──────────────────┘└────┘ ┴
typ └────┘ └──────────────────┘└────┘└┘┴
doc └────┘ └────┘ ┴
txt └────┘ └────┘ ┴
par └────┘ └────┘ ┴
pid ┴ └────┘ ┴
st ─────────────────────────────────────────┘└┘└
173 exact hx },
id └┘
src └────┘ ┴
typ └────┘└┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────┘└┘└
174 assume x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────┘└─
175 have : continuous_within_at (λ r, B x + r * (x - a)) (Ioi 0) 0,
id └──────────────────┘ ┴ ┴ ┴ └─┘
src └─────┘└──────────────────┘┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘└───┘
typ └─────┘└──────────────────┘┴ └──┘┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴└─┘ └─┘└───┘
doc └─────┘└──────────────────┘┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘└───┘
txt └─────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └───┘
par └─────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └───┘
pid └───┘└┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──┘┴
st ───────────────────────────────────────────────────────────────┘└─
176 from continuous_within_at_const.add (continuous_within_at_id.mul continuous_within_at_const),
id └────────────────────────────┘ └─────────────────────────┘ └────────────────────────┘
src └───┘└────────────────────────────┘┴ └─────────────────────────┘┴└────────────────────────┘┴
typ └───┘└────────────────────────────┘┴ └─────────────────────────┘┴└────────────────────────┘┴
doc └───┘ ┴ ┴ ┴
txt └───┘ ┴ ┴ ┴
par └───┘ ┴ ┴ ┴
pid └───┘ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
177 convert continuous_within_at_const.closure_le _ this (Hr x hx); simp [closure_Ioi]
id └───────────────────────────────────┘ └──┘ └┘ ┴ └┘ └─────────┘
src └──────┘└───────────────────────────────────┘└─┘ ┴ ┴ ┴ ┴ └────┘└─────────┘└┘
typ └──────┘└───────────────────────────────────┘└─┘└──┘┴ └┘┴┴┴└┘┴ └────┘└─────────┘└┘
doc └──────┘ └─┘ ┴ ┴ ┴ ┴ └────┘└─────────┘└┘
txt └──────┘ └─┘ ┴ ┴ ┴ ┴ └────┘ └┘
par └──────┘ └─┘ ┴ ┴ ┴ ┴ └────┘ └┘
pid ┴ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴
st ────────────────────────────────────────────────────────────────────────────────────┘
178 end
st └─┘
179
180 /-- General fencing theorem for continuous functions with an estimate on the derivative.
181 Let `f` and `B` be continuous functions on `[a, b]` such that
182
183 * `f a ≤ B a`;
184 * `B` has right derivative `B'` at every point of `[a, b)`;
185 * `f` has right derivative `f'` at every point of `[a, b)`;
186 * we have `f' x < B' x` whenever `f x = B x`.
187
188 Then `f x ≤ B x` everywhere on `[a, b]`. -/
189 lemma image_le_of_deriv_right_lt_deriv_boundary' {f f' : ℝ → ℝ} {a b : ℝ}
id ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴
190 (hf : continuous_on f (Icc a b))
id └───────────┘ ┴ └─┘ ┴ ┴
src └───────────┘ └─┘
typ └───────────┘ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
191 (hf' : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ioi x) x)
id ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
src └─┘ └─────────────────┘ └─┘
typ ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
doc └─┘ └─────────────────┘ └─┘
192 {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : continuous_on B (Icc a b))
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ └─┘ ┴ ┴
src ┴ ┴ ┴ └───────────┘ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
193 (hB' : ∀ x ∈ Ico a b, has_deriv_within_at B (B' x) (Ioi x) x)
id ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
src └─┘ └─────────────────┘ └─┘
typ ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
doc └─┘ └─────────────────┘ └─┘
194 (bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x) :
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └─┘ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └─┘
195 ∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x :=
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
196 image_le_of_liminf_slope_right_lt_deriv_boundary' hf
id └───────────────────────────────────────────────┘ └┘
src └───────────────────────────────────────────────┘
typ └───────────────────────────────────────────────┘ └┘
doc └───────────────────────────────────────────────┘
197 (λ x hx r hr, (hf' x hx).liminf_right_slope_le hr) ha hB hB' bound
id ┴ └┘ ┴ └┘ └─┘ ┴ └┘ └───────────────────┘ └┘ └┘ └┘ └─┘ └───┘
src └───────────────────┘
typ ┴ └┘ ┴ └┘ └─┘ ┴ └┘ └───────────────────┘ └┘ └┘ └┘ └─┘ └───┘
198
199 /-- General fencing theorem for continuous functions with an estimate on the derivative.
200 Let `f` and `B` be continuous functions on `[a, b]` such that
201
202 * `f a ≤ B a`;
203 * `B` has derivative `B'` everywhere on `ℝ`;
204 * `f` has right derivative `f'` at every point of `[a, b)`;
205 * we have `f' x < B' x` whenever `f x = B x`.
206
207 Then `f x ≤ B x` everywhere on `[a, b]`. -/
208 lemma image_le_of_deriv_right_lt_deriv_boundary {f f' : ℝ → ℝ} {a b : ℝ}
id ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴
209 (hf : continuous_on f (Icc a b))
id └───────────┘ ┴ └─┘ ┴ ┴
src └───────────┘ └─┘
typ └───────────┘ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
210 (hf' : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ioi x) x)
id ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
src └─┘ └─────────────────┘ └─┘
typ ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
doc └─┘ └─────────────────┘ └─┘
211 {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : ∀ x, has_deriv_at B (B' x) x)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ └┘ ┴ ┴
src ┴ ┴ ┴ └──────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ └┘ ┴ ┴
doc └──────────┘
212 (bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x) :
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └─┘ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └─┘
213 ∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x :=
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
214 image_le_of_deriv_right_lt_deriv_boundary' hf hf' ha
id └────────────────────────────────────────┘ └┘ └─┘ └┘
src └────────────────────────────────────────┘
typ └────────────────────────────────────────┘ └┘ └─┘ └┘
doc └────────────────────────────────────────┘
215 (λ x hx, (hB x).continuous_at.continuous_within_at)
id ┴ └┘ └┘ ┴ └───────────┘ └──────────────────┘
src └───────────┘ └──────────────────┘
typ ┴ └┘ └┘ ┴ └───────────┘ └──────────────────┘
216 (λ x hx, (hB x).has_deriv_within_at) bound
id ┴ └┘ └┘ ┴ └─────────────────┘ └───┘
src └─────────────────┘
typ ┴ └┘ └┘ ┴ └─────────────────┘ └───┘
217
218 /-- General fencing theorem for continuous functions with an estimate on the derivative.
219 Let `f` and `B` be continuous functions on `[a, b]` such that
220
221 * `f a ≤ B a`;
222 * `B` has derivative `B'` everywhere on `ℝ`;
223 * `f` has right derivative `f'` at every point of `[a, b)`;
224 * we have `f' x ≤ B' x` on `[a, b)`.
225
226 Then `f x ≤ B x` everywhere on `[a, b]`. -/
227 lemma image_le_of_deriv_right_le_deriv_boundary {f f' : ℝ → ℝ} {a b : ℝ}
id ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴
228 (hf : continuous_on f (Icc a b))
id └───────────┘ ┴ └─┘ ┴ ┴
src └───────────┘ └─┘
typ └───────────┘ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
229 (hf' : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ioi x) x)
id ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
src └─┘ └─────────────────┘ └─┘
typ ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
doc └─┘ └─────────────────┘ └─┘
230 {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : continuous_on B (Icc a b))
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ └─┘ ┴ ┴
src ┴ ┴ ┴ └───────────┘ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
231 (hB' : ∀ x ∈ Ico a b, has_deriv_within_at B (B' x) (Ioi x) x)
id ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
src └─┘ └─────────────────┘ └─┘
typ ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
doc └─┘ └─────────────────┘ └─┘
232 (bound : ∀ x ∈ Ico a b, f' x ≤ B' x) :
id ┴ └─┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └─┘ ┴
typ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └─┘
233 ∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x :=
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
234 image_le_of_liminf_slope_right_le_deriv_boundary hf ha hB hB' $
id └──────────────────────────────────────────────┘ └┘ └┘ └┘ └─┘
src └──────────────────────────────────────────────┘
typ └──────────────────────────────────────────────┘ └┘ └┘ └┘ └─┘
doc └──────────────────────────────────────────────┘
235 assume x hx r hr, (hf' x hx).liminf_right_slope_le (lt_of_le_of_lt (bound x hx) hr)
id ┴ └┘ ┴ └┘ └─┘ ┴ └┘ └───────────────────┘ └────────────┘ └───┘ ┴ └┘ └┘
src └───────────────────┘ └────────────┘
typ ┴ └┘ ┴ └┘ └─┘ ┴ └┘ └───────────────────┘ └────────────┘ └───┘ ┴ └┘ └┘
236
237 /-! ### Vector-valued functions `f : ℝ → E` -/
238
239 section
240
241 variables {f : ℝ → E} {a b : ℝ}
id ┴ ┴
src ┴ ┴
typ ┴ ┴
242
243 /-- General fencing theorem for continuous functions with an estimate on the derivative.
244 Let `f` and `B` be continuous functions on `[a, b]` such that
245
246 * `∥f a∥ ≤ B a`;
247 * `B` has right derivative at every point of `[a, b)`;
248 * for each `x ∈ [a, b)` the right-side limit inferior of `(∥f z∥ - ∥f x∥) / (z - x)`
249 is bounded above by a function `f'`;
250 * we have `f' x < B' x` whenever `∥f x∥ = B x`.
251
252 Then `∥f x∥ ≤ B x` everywhere on `[a, b]`. -/
253 lemma image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary {E : Type*} [normed_group E]
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
doc └──────────┘
254 {f : ℝ → E} {f' : ℝ → ℝ} (hf : continuous_on f (Icc a b))
id ┴ ┴ ┴ ┴ └───────────┘ ┴ └─┘ ┴ ┴
src ┴ ┴ ┴ └───────────┘ └─┘
typ ┴ ┴ ┴ ┴ └───────────┘ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
255 -- `hf'` actually says `liminf ∥z - x∥⁻¹ * (∥f z∥ - ∥f x∥) ≤ f' x`
256 (hf' : ∀ x ∈ Ico a b, ∀ r, f' x < r →
id ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
doc └─┘
257 ∃ᶠ z in nhds_within x (Ioi x), (z - x)⁻¹ * (∥f z∥ - ∥f x∥) < r)
id └┘ ┴ └┘ └─────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴┴ ┴ ┴
src └┘ └┘ └─────────┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ └┘ └─────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴┴ ┴ ┴
doc └┘ └┘ └─────────┘ └─┘ ┴
258 {B B' : ℝ → ℝ} (ha : ∥f a∥ ≤ B a) (hB : continuous_on B (Icc a b))
id ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └───────────┘ ┴ └─┘ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └───────────┘ └─┘
typ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └───────────┘ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
259 (hB' : ∀ x ∈ Ico a b, has_deriv_within_at B (B' x) (Ioi x) x)
id ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
src └─┘ └─────────────────┘ └─┘
typ ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
doc └─┘ └─────────────────┘ └─┘
260 (bound : ∀ x ∈ Ico a b, ∥f x∥ = B x → f' x < B' x) :
id ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └─┘ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └─┘
261 ∀ ⦃x⦄, x ∈ Icc a b → ∥f x∥ ≤ B x :=
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
doc └─┘
262 image_le_of_liminf_slope_right_lt_deriv_boundary' (continuous_norm.comp_continuous_on hf) hf'
id └───────────────────────────────────────────────┘ └─────────────┘└─────────────────┘ └┘ └─┘
src └───────────────────────────────────────────────┘ └─────────────┘└─────────────────┘
typ └───────────────────────────────────────────────┘ └─────────────┘└─────────────────┘ └┘ └─┘
doc └───────────────────────────────────────────────┘
263 ha hB hB' bound
id └┘ └┘ └─┘ └───┘
typ └┘ └┘ └─┘ └───┘
264
265 /-- General fencing theorem for continuous functions with an estimate on the norm of the derivative.
266 Let `f` and `B` be continuous functions on `[a, b]` such that
267
268 * `∥f a∥ ≤ B a`;
269 * `f` and `B` have right derivatives `f'` and `B'` respectively at every point of `[a, b)`;
270 * the norm of `f'` is strictly less than `B'` whenever `∥f x∥ = B x`.
271
272 Then `∥f x∥ ≤ B x` everywhere on `[a, b]`. We use one-sided derivatives in the assumptions
273 to make this theorem work for piecewise differentiable functions.
274 -/
275 lemma image_norm_le_of_norm_deriv_right_lt_deriv_boundary' {f' : ℝ → E}
id ┴ ┴
src ┴
typ ┴ ┴
276 (hf : continuous_on f (Icc a b))
id └───────────┘ ┴ └─┘ ┴ ┴
src └───────────┘ └─┘
typ └───────────┘ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
277 (hf' : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ioi x) x)
id ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
src └─┘ └─────────────────┘ └─┘
typ ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
doc └─┘ └─────────────────┘ └─┘
278 {B B' : ℝ → ℝ} (ha : ∥f a∥ ≤ B a) (hB : continuous_on B (Icc a b))
id ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └───────────┘ ┴ └─┘ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └───────────┘ └─┘
typ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └───────────┘ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
279 (hB' : ∀ x ∈ Ico a b, has_deriv_within_at B (B' x) (Ioi x) x)
id ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
src └─┘ └─────────────────┘ └─┘
typ ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
doc └─┘ └─────────────────┘ └─┘
280 (bound : ∀ x ∈ Ico a b, ∥f x∥ = B x → ∥f' x∥ < B' x) :
id ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴└┘ ┴┴ ┴ └┘ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴└┘ ┴┴ ┴ └┘ ┴
doc └─┘
281 ∀ ⦃x⦄, x ∈ Icc a b → ∥f x∥ ≤ B x :=
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
doc └─┘
282 image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary hf
id └────────────────────────────────────────────────────────┘ └┘
src └────────────────────────────────────────────────────────┘
typ └────────────────────────────────────────────────────────┘ └┘
doc └────────────────────────────────────────────────────────┘
283 (λ x hx r hr, (hf' x hx).liminf_right_slope_norm_le hr) ha hB hB' bound
id ┴ └┘ ┴ └┘ └─┘ ┴ └┘ └────────────────────────┘ └┘ └┘ └┘ └─┘ └───┘
src └────────────────────────┘
typ ┴ └┘ ┴ └┘ └─┘ ┴ └┘ └────────────────────────┘ └┘ └┘ └┘ └─┘ └───┘
doc └────────────────────────┘
284
285 /-- General fencing theorem for continuous functions with an estimate on the norm of the derivative.
286 Let `f` and `B` be continuous functions on `[a, b]` such that
287
288 * `∥f a∥ ≤ B a`;
289 * `f` has right derivative `f'` at every point of `[a, b)`;
290 * `B` has derivative `B'` everywhere on `ℝ`;
291 * the norm of `f'` is strictly less than `B'` whenever `∥f x∥ = B x`.
292
293 Then `∥f x∥ ≤ B x` everywhere on `[a, b]`. We use one-sided derivatives in the assumptions
294 to make this theorem work for piecewise differentiable functions.
295 -/
296 lemma image_norm_le_of_norm_deriv_right_lt_deriv_boundary {f' : ℝ → E}
id ┴ ┴
src ┴
typ ┴ ┴
297 (hf : continuous_on f (Icc a b))
id └───────────┘ ┴ └─┘ ┴ ┴
src └───────────┘ └─┘
typ └───────────┘ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
298 (hf' : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ioi x) x)
id ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
src └─┘ └─────────────────┘ └─┘
typ ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
doc └─┘ └─────────────────┘ └─┘
299 {B B' : ℝ → ℝ} (ha : ∥f a∥ ≤ B a) (hB : ∀ x, has_deriv_at B (B' x) x)
id ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ └┘ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └──────────┘
typ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ └┘ ┴ ┴
doc └──────────┘
300 (bound : ∀ x ∈ Ico a b, ∥f x∥ = B x → ∥f' x∥ < B' x) :
id ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴└┘ ┴┴ ┴ └┘ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴└┘ ┴┴ ┴ └┘ ┴
doc └─┘
301 ∀ ⦃x⦄, x ∈ Icc a b → ∥f x∥ ≤ B x :=
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
doc └─┘
302 image_norm_le_of_norm_deriv_right_lt_deriv_boundary' hf hf' ha
id └──────────────────────────────────────────────────┘ └┘ └─┘ └┘
src └──────────────────────────────────────────────────┘
typ └──────────────────────────────────────────────────┘ └┘ └─┘ └┘
doc └──────────────────────────────────────────────────┘
303 (λ x hx, (hB x).continuous_at.continuous_within_at)
id ┴ └┘ └┘ ┴ └───────────┘ └──────────────────┘
src └───────────┘ └──────────────────┘
typ ┴ └┘ └┘ ┴ └───────────┘ └──────────────────┘
304 (λ x hx, (hB x).has_deriv_within_at) bound
id ┴ └┘ └┘ ┴ └─────────────────┘ └───┘
src └─────────────────┘
typ ┴ └┘ └┘ ┴ └─────────────────┘ └───┘
305
306 /-- General fencing theorem for continuous functions with an estimate on the norm of the derivative.
307 Let `f` and `B` be continuous functions on `[a, b]` such that
308
309 * `∥f a∥ ≤ B a`;
310 * `f` and `B` have right derivatives `f'` and `B'` respectively at every point of `[a, b)`;
311 * we have `∥f' x∥ ≤ B x` everywhere on `[a, b)`.
312
313 Then `∥f x∥ ≤ B x` everywhere on `[a, b]`. We use one-sided derivatives in the assumptions
314 to make this theorem work for piecewise differentiable functions.
315 -/
316 lemma image_norm_le_of_norm_deriv_right_le_deriv_boundary' {f' : ℝ → E}
id ┴ ┴
src ┴
typ ┴ ┴
317 (hf : continuous_on f (Icc a b))
id └───────────┘ ┴ └─┘ ┴ ┴
src └───────────┘ └─┘
typ └───────────┘ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
318 (hf' : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ioi x) x)
id ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
src └─┘ └─────────────────┘ └─┘
typ ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
doc └─┘ └─────────────────┘ └─┘
319 {B B' : ℝ → ℝ} (ha : ∥f a∥ ≤ B a) (hB : continuous_on B (Icc a b))
id ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └───────────┘ ┴ └─┘ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └───────────┘ └─┘
typ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └───────────┘ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
320 (hB' : ∀ x ∈ Ico a b, has_deriv_within_at B (B' x) (Ioi x) x)
id ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
src └─┘ └─────────────────┘ └─┘
typ ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
doc └─┘ └─────────────────┘ └─┘
321 (bound : ∀ x ∈ Ico a b, ∥f' x∥ ≤ B' x) :
id ┴ └─┘ ┴ ┴ ┴└┘ ┴┴ ┴ └┘ ┴
src └─┘ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴└┘ ┴┴ ┴ └┘ ┴
doc └─┘
322 ∀ ⦃x⦄, x ∈ Icc a b → ∥f x∥ ≤ B x :=
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
doc └─┘
323 image_le_of_liminf_slope_right_le_deriv_boundary (continuous_norm.comp_continuous_on hf) ha hB hB' $
id └──────────────────────────────────────────────┘ └─────────────┘└─────────────────┘ └┘ └┘ └┘ └─┘
src └──────────────────────────────────────────────┘ └─────────────┘└─────────────────┘
typ └──────────────────────────────────────────────┘ └─────────────┘└─────────────────┘ └┘ └┘ └┘ └─┘
doc └──────────────────────────────────────────────┘
324 (λ x hx r hr, (hf' x hx).liminf_right_slope_norm_le (lt_of_le_of_lt (bound x hx) hr))
id ┴ └┘ ┴ └┘ └─┘ ┴ └┘ └────────────────────────┘ └────────────┘ └───┘ ┴ └┘ └┘
src └────────────────────────┘ └────────────┘
typ ┴ └┘ ┴ └┘ └─┘ ┴ └┘ └────────────────────────┘ └────────────┘ └───┘ ┴ └┘ └┘
doc └────────────────────────┘
325
326 /-- General fencing theorem for continuous functions with an estimate on the norm of the derivative.
327 Let `f` and `B` be continuous functions on `[a, b]` such that
328
329 * `∥f a∥ ≤ B a`;
330 * `f` has right derivative `f'` at every point of `[a, b)`;
331 * `B` has derivative `B'` everywhere on `ℝ`;
332 * we have `∥f' x∥ ≤ B x` everywhere on `[a, b)`.
333
334 Then `∥f x∥ ≤ B x` everywhere on `[a, b]`. We use one-sided derivatives in the assumptions
335 to make this theorem work for piecewise differentiable functions.
336 -/
337 lemma image_norm_le_of_norm_deriv_right_le_deriv_boundary {f' : ℝ → E}
id ┴ ┴
src ┴
typ ┴ ┴
338 (hf : continuous_on f (Icc a b))
id └───────────┘ ┴ └─┘ ┴ ┴
src └───────────┘ └─┘
typ └───────────┘ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
339 (hf' : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ioi x) x)
id ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
src └─┘ └─────────────────┘ └─┘
typ ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
doc └─┘ └─────────────────┘ └─┘
340 {B B' : ℝ → ℝ} (ha : ∥f a∥ ≤ B a) (hB : ∀ x, has_deriv_at B (B' x) x)
id ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ └┘ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └──────────┘
typ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ └┘ ┴ ┴
doc └──────────┘
341 (bound : ∀ x ∈ Ico a b, ∥f' x∥ ≤ B' x) :
id ┴ └─┘ ┴ ┴ ┴└┘ ┴┴ ┴ └┘ ┴
src └─┘ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴└┘ ┴┴ ┴ └┘ ┴
doc └─┘
342 ∀ ⦃x⦄, x ∈ Icc a b → ∥f x∥ ≤ B x :=
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
doc └─┘
343 image_norm_le_of_norm_deriv_right_le_deriv_boundary' hf hf' ha
id └──────────────────────────────────────────────────┘ └┘ └─┘ └┘
src └──────────────────────────────────────────────────┘
typ └──────────────────────────────────────────────────┘ └┘ └─┘ └┘
doc └──────────────────────────────────────────────────┘
344 (λ x hx, (hB x).continuous_at.continuous_within_at)
id ┴ └┘ └┘ ┴ └───────────┘ └──────────────────┘
src └───────────┘ └──────────────────┘
typ ┴ └┘ └┘ ┴ └───────────┘ └──────────────────┘
345 (λ x hx, (hB x).has_deriv_within_at) bound
id ┴ └┘ └┘ ┴ └─────────────────┘ └───┘
src └─────────────────┘
typ ┴ └┘ └┘ ┴ └─────────────────┘ └───┘
346
347 /-- A function on `[a, b]` with the norm of the right derivative bounded by `C`
348 satisfies `∥f x - f a∥ ≤ C * (x - a)`. -/
349 theorem norm_image_sub_le_of_norm_deriv_right_le_segment {f' : ℝ → E} {C : ℝ}
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
350 (hf : continuous_on f (Icc a b))
id └───────────┘ ┴ └─┘ ┴ ┴
src └───────────┘ └─┘
typ └───────────┘ ┴ └─┘ ┴ ┴
doc └───────────┘ └─┘
351 (hf' : ∀ x ∈ Ico a b, has_deriv_within_at f (f' x) (Ioi x) x)
id ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
src └─┘ └─────────────────┘ └─┘
typ ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
doc └─┘ └─────────────────┘ └─┘
352 (bound : ∀x ∈ Ico a b, ∥f' x∥ ≤ C) :
id ┴ └─┘ ┴ ┴ ┴└┘ ┴┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴└┘ ┴┴ ┴ ┴
doc └─┘
353 ∀ x ∈ Icc a b, ∥f x - f a∥ ≤ C * (x - a) :=
id ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
354 begin
st └─────
355 let g := λ x, f x - f a,
id ┴ ┴ ┴
src └───────┘ └──┘ ┴ ┴┴┴ ┴
typ └───────┘ └──┘ ┴ ┴┴┴┴┴┴
doc └───────┘ └──┘ ┴ ┴ ┴ ┴
txt └───────┘ └──┘ ┴ ┴ ┴ ┴
par └───────┘ └──┘ ┴ ┴ ┴ ┴
pid └───┘┴└─┘ └──┘ ┴ ┴ ┴ ┴
st ────────────────────────┘└─
356 have hg : continuous_on g (Icc a b), from hf.sub continuous_on_const,
id └───────────┘ ┴ └─┘ ┴ ┴ └────┘ └─────────────────┘
src └────────┘└───────────┘┴ ┴ └─┘┴ ┴ ┴ └───┘└────┘┴└─────────────────┘
typ └────────┘└───────────┘┴┴┴ └─┘┴┴┴┴┴ └───┘└────┘┴└─────────────────┘
doc └────────┘└───────────┘┴ ┴ └─┘┴ ┴ ┴ └───┘ ┴
txt └────────┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
par └────────┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
pid └─────┘└─┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
st ────────────────────────────────────┘└───────────────────────────────┘└─
357 have hg' : ∀ x ∈ Ico a b, has_deriv_within_at g (f' x) (Ioi x) x,
id └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ └─┘
src └─────────┘ └───┘└─┘┴ ┴ ┴└─────────────────┘┴ ┴ ┴ └┘ └─┘┴ └┘
typ └─────────┘ └───┘└─┘┴┴┴┴ ┴└─────────────────┘┴┴┴ └┘┴ └┘ └─┘┴ └┘
doc └─────────┘ └───┘└─┘┴ ┴ ┴└─────────────────┘┴ ┴ ┴ └┘ └─┘┴ └┘
txt └─────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘
par └─────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘
pid └──────┘└─┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘
st ─────────────────────────────────────────────────────────────────┘└─
358 { assume x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───┘└─────────┘└─
359 simpa using (hf' x hx).sub (has_deriv_within_at_const _ _ _) },
id └─┘ ┴ └┘ └───────────────────────┘
src └──────────┘ ┴ ┴ └────┘ └───────────────────────┘└──────┘
typ └──────────┘ └─┘┴┴┴└┘└────┘ └───────────────────────┘└──────┘
doc └──────────┘ ┴ ┴ └────┘ └──────┘
txt └──────────┘ ┴ ┴ └────┘ └──────┘
par └──────────┘ ┴ ┴ └────┘ └──────┘
pid ┴└────┘ ┴ ┴ └────┘ └─────┘┴
st ────────────────────────────────────────────────────────────────┘└┘└
360 let B := λ x, C * (x - a),
id ┴ ┴ ┴
src └───────┘ └──┘ ┴┴┴ ┴ ┴ ┴
typ └───────┘ └──┘┴┴┴┴ ┴ ┴┴┴
doc └───────┘ └──┘ ┴ ┴ ┴ ┴ ┴
txt └───────┘ └──┘ ┴ ┴ ┴ ┴ ┴
par └───────┘ └──┘ ┴ ┴ ┴ ┴ ┴
pid └───┘┴└─┘ └──┘ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────┘└─
361 have hB : ∀ x, has_deriv_at B C x,
id └──────────┘ ┴ ┴
src └────────┘ └┘ ┴└──────────┘┴ ┴ ┴
typ └────────┘ └┘ ┴└──────────┘┴┴┴┴┴
doc └────────┘ └┘ ┴└──────────┘┴ ┴ ┴
txt └────────┘ └┘ ┴ ┴ ┴ ┴
par └────────┘ └┘ ┴ ┴ ┴ ┴
pid └─────┘└─┘ └┘ ┴ ┴ ┴ ┴
st ──────────────────────────────────┘└─
362 { assume x,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───┘└──────┘└─
363 simpa using (has_deriv_at_const x C).mul ((has_deriv_at_id x).sub (has_deriv_at_const x a)) },
id ┴ └─────────────┘ └────────────────┘ ┴ ┴
src └──────────┘ ┴ ┴ └────┘ └─────────────┘┴ └────┘ └────────────────┘┴ ┴ └─┘
typ └──────────┘ ┴ ┴┴└────┘ └─────────────┘┴ └────┘ └────────────────┘┴┴┴┴└─┘
doc └──────────┘ ┴ ┴ └────┘ ┴ └────┘ ┴ ┴ └─┘
txt └──────────┘ ┴ ┴ └────┘ ┴ └────┘ ┴ ┴ └─┘
par └──────────┘ ┴ ┴ └────┘ ┴ └────┘ ┴ ┴ └─┘
pid ┴└────┘ ┴ ┴ └────┘ ┴ └────┘ ┴ ┴ └┘┴
st ───────────────────────────────────────────────────────────────────────────────────────────────┘└┘└
364 convert image_norm_le_of_norm_deriv_right_le_deriv_boundary hg hg' _ hB bound,
id └─────────────────────────────────────────────────┘ └┘ └─┘ └┘ └───┘
src └──────┘└─────────────────────────────────────────────────┘┴ ┴ └─┘ ┴
typ └──────┘└─────────────────────────────────────────────────┘┴└┘┴└─┘└─┘└┘┴└───┘
doc └──────┘└─────────────────────────────────────────────────┘┴ ┴ └─┘ ┴
txt └──────┘ ┴ ┴ └─┘ ┴
par └──────┘ ┴ ┴ └─┘ ┴
pid ┴ ┴ ┴ └─┘ ┴
st ──────────────────────────────────────────────────────────────────────────────┘└─
365 { simp only [g, B] },
id ┴ ┴
src └─────────┘ └┘ └┘
typ └─────────┘┴└┘┴└┘
doc └─────────┘ └┘ └┘
txt └─────────┘ └┘ └┘
par └─────────┘ └┘ └┘
pid ┴└──┘└┘ └┘ ┴┴
st ───┘└───────────────┘└┘└
366 { simp only [g, B], rw [sub_self, _root_.norm_zero, sub_self, mul_zero] }
id ┴ ┴ └──────┘ └──────────────┘ └──────┘ └──────┘
src └─────────┘ └┘ ┴ └──┘└──────┘└┘└──────────────┘└┘└──────┘└┘└──────┘└┘
typ └─────────┘┴└┘┴┴ └──┘└──────┘└┘└──────────────┘└┘└──────┘└┘└──────┘└┘
doc └─────────┘ └┘ ┴ └──┘ └┘ └┘ └┘ └┘
txt └─────────┘ └┘ ┴ └──┘ └┘ └┘ └┘ └┘
par └─────────┘ └┘ ┴ └──┘ └┘ └┘ └┘ └┘
pid ┴└──┘└┘ └┘ ┴ └┘ └┘ └┘ └┘ ┴┴
st ───────────────────┘└────────────┘└────────────────┘└────────┘└────────┘┴┴└─
367 end
st ──┘
368
369 /-- A function on `[a, b]` with the norm of the derivative within `[a, b]`
370 bounded by `C` satisfies `∥f x - f a∥ ≤ C * (x - a)`, `has_deriv_within_at`
371 version. -/
372 theorem norm_image_sub_le_of_norm_deriv_le_segment' {f' : ℝ → E} {C : ℝ}
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
373 (hf : ∀ x ∈ Icc a b, has_deriv_within_at f (f' x) (Icc a b) x)
id ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴
src └─┘ └─────────────────┘ └─┘
typ ┴ └─┘ ┴ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴
doc └─┘ └─────────────────┘ └─┘
374 (bound : ∀x ∈ Ico a b, ∥f' x∥ ≤ C) :
id ┴ └─┘ ┴ ┴ ┴└┘ ┴┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴└┘ ┴┴ ┴ ┴
doc └─┘
375 ∀ x ∈ Icc a b, ∥f x - f a∥ ≤ C * (x - a) :=
id ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
376 begin
st └─────
377 refine norm_image_sub_le_of_norm_deriv_right_le_segment
id └──────────────────────────────────────────────┘
src └─────┘└──────────────────────────────────────────────┘└
typ └─────┘└──────────────────────────────────────────────┘└
doc └─────┘└──────────────────────────────────────────────┘└
txt └─────┘ └
par └─────┘ └
pid ┴ └
st ──────────────────────────────────────────────────────────
378 (λ x hx, (hf x hx).continuous_within_at) (λ x hx, _) bound,
id └┘ └───┘
src ───┘ └─────┘ ┴ ┴ └──────────────────────┘ └────────┘
typ ───┘ └─────┘ └┘┴ ┴ └──────────────────────┘ └────────┘└───┘
doc ───┘ └─────┘ ┴ ┴ └──────────────────────┘ └────────┘
txt ───┘ └─────┘ ┴ ┴ └──────────────────────┘ └────────┘
par ───┘ └─────┘ ┴ ┴ └──────────────────────┘ └────────┘
pid ───┘ └─────┘ ┴ ┴ └──────────────────────┘ └────────┘
st ─────────────────────────────────────────────────────────────┘└─
379 apply (hf x $ Ico_subset_Icc_self hx).nhds_within,
id └┘ ┴ └─────────────────┘ └┘
src └────┘ ┴ ┴ ┴└─────────────────┘┴ └───────────┘
typ └────┘ └┘┴┴┴ ┴└─────────────────┘┴└┘└───────────┘
doc └────┘ ┴ ┴ ┴ ┴ └───────────┘
txt └────┘ ┴ ┴ ┴ ┴ └───────────┘
par └────┘ ┴ ┴ ┴ ┴ └───────────┘
pid ┴ ┴ ┴ ┴ ┴ └──────────┘┴
st ──────────────────────────────────────────────────┘└─
380 exact Icc_mem_nhds_within_Ioi hx
id └─────────────────────┘ └┘
src └────┘└─────────────────────┘┴ ┴
typ └────┘└─────────────────────┘┴└┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────────────────────┘
381 end
st └─┘
382
383 /-- A function on `[a, b]` with the norm of the derivative within `[a, b]`
384 bounded by `C` satisfies `∥f x - f a∥ ≤ C * (x - a)`, `deriv_within`
385 version. -/
386 theorem norm_image_sub_le_of_norm_deriv_le_segment {C : ℝ} (hf : differentiable_on ℝ f (Icc a b))
id ┴ └───────────────┘ ┴ ┴ └─┘ ┴ ┴
src ┴ └───────────────┘ ┴ └─┘
typ ┴ └───────────────┘ ┴ ┴ └─┘ ┴ ┴
doc └───────────────┘ └─┘
387 (bound : ∀x ∈ Ico a b, ∥deriv_within f (Icc a b) x∥ ≤ C) :
id ┴ └─┘ ┴ ┴ ┴└──────────┘ ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴
src └─┘ ┴└──────────┘ └─┘ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴└──────────┘ ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴
doc └─┘ └──────────┘ └─┘
388 ∀ x ∈ Icc a b, ∥f x - f a∥ ≤ C * (x - a) :=
id ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
389 begin
st └─────
390 refine norm_image_sub_le_of_norm_deriv_le_segment' _ bound,
id └─────────────────────────────────────────┘ └───┘
src └─────┘└─────────────────────────────────────────┘└─┘
typ └─────┘└─────────────────────────────────────────┘└─┘└───┘
doc └─────┘└─────────────────────────────────────────┘└─┘
txt └─────┘ └─┘
par └─────┘ └─┘
pid ┴ └─┘
st ───────────────────────────────────────────────────────────┘└─
391 exact λ x hx, (hf x hx).has_deriv_within_at
id └┘
src └────┘ └─────┘ ┴ └┘ └────────────────────┘
typ └────┘ └─────┘ └┘┴ └┘ └────────────────────┘
doc └────┘ └─────┘ ┴ └┘ └────────────────────┘
txt └────┘ └─────┘ ┴ └┘ └────────────────────┘
par └────┘ └─────┘ ┴ └┘ └────────────────────┘
pid ┴ └─────┘ ┴ └┘ └──────────────────┘└┘
st ──────────────────────────────────────────────┘
392 end
st └─┘
393
394 /-- A function on `[0, 1]` with the norm of the derivative within `[0, 1]`
395 bounded by `C` satisfies `∥f 1 - f 0∥ ≤ C`, `has_deriv_within_at`
396 version. -/
397 theorem norm_image_sub_le_of_norm_deriv_le_segment_01' {f' : ℝ → E} {C : ℝ}
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
398 (hf : ∀ x ∈ Icc (0:ℝ) 1, has_deriv_within_at f (f' x) (Icc (0:ℝ) 1) x)
id ┴ └─┘ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
src └─┘ ┴ └─────────────────┘ └─┘ ┴
typ ┴ └─┘ ┴ └─────────────────┘ ┴ └┘ ┴ └─┘ ┴ ┴
doc └─┘ └─────────────────┘ └─┘
399 (bound : ∀x ∈ Ico (0:ℝ) 1, ∥f' x∥ ≤ C) :
id ┴ └─┘ ┴ ┴└┘ ┴┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴└┘ ┴┴ ┴ ┴
doc └─┘
400 ∥f 1 - f 0∥ ≤ C :=
id ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴
401 by simpa only [sub_zero, mul_one]
id └──────┘ └─────┘
src └──────────┘└──────┘└┘└─────┘└─
typ └──────────┘└──────┘└┘└─────┘└─
doc └──────────┘ └┘ └─
txt └──────────┘ └┘ └─
par └──────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └───────────────────────────────
402 using norm_image_sub_le_of_norm_deriv_le_segment' hf bound 1 (right_mem_Icc.2 zero_le_one)
id └─────────────────────────────────────────┘ └┘ └───┘ └───────────┘ └─────────┘
src ───────┘└─────────────────────────────────────────┘┴ ┴ └─┘ └───────────┘└─┘└─────────┘└─
typ ───────┘└─────────────────────────────────────────┘┴└┘┴└───┘└─┘ └───────────┘└─┘└─────────┘└─
doc ───────┘└─────────────────────────────────────────┘┴ ┴ └─┘ └─┘ └─
txt ───────┘ ┴ ┴ └─┘ └─┘ └─
par ───────┘ ┴ ┴ └─┘ └─┘ └─
pid ─┘└────┘ ┴ ┴ └─┘ └─┘ ┴└
st ─────────────────────────────────────────────────────────────────────────────────────────────
403
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
404 /-- A function on `[0, 1]` with the norm of the derivative within `[0, 1]`
405 bounded by `C` satisfies `∥f 1 - f 0∥ ≤ C`, `deriv_within` version. -/
406 theorem norm_image_sub_le_of_norm_deriv_le_segment_01 {C : ℝ}
id ┴
src ┴
typ ┴
407 (hf : differentiable_on ℝ f (Icc (0:ℝ) 1))
id └───────────────┘ ┴ ┴ └─┘ ┴
src └───────────────┘ ┴ └─┘ ┴
typ └───────────────┘ ┴ ┴ └─┘ ┴
doc └───────────────┘ └─┘
408 (bound : ∀x ∈ Ico (0:ℝ) 1, ∥deriv_within f (Icc (0:ℝ) 1) x∥ ≤ C) :
id ┴ └─┘ ┴ ┴└──────────┘ ┴ └─┘ ┴ ┴┴ ┴ ┴
src └─┘ ┴ ┴└──────────┘ └─┘ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴└──────────┘ ┴ └─┘ ┴ ┴┴ ┴ ┴
doc └─┘ └──────────┘ └─┘
409 ∥f 1 - f 0∥ ≤ C :=
id ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴
410 by simpa only [sub_zero, mul_one]
id └──────┘ └─────┘
src └──────────┘└──────┘└┘└─────┘└─
typ └──────────┘└──────┘└┘└─────┘└─
doc └──────────┘ └┘ └─
txt └──────────┘ └┘ └─
par └──────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └───────────────────────────────
411 using norm_image_sub_le_of_norm_deriv_le_segment hf bound 1 (right_mem_Icc.2 zero_le_one)
id └────────────────────────────────────────┘ └┘ └───┘ └───────────┘ └─────────┘
src ───────┘└────────────────────────────────────────┘┴ ┴ └─┘ └───────────┘└─┘└─────────┘└─
typ ───────┘└────────────────────────────────────────┘┴└┘┴└───┘└─┘ └───────────┘└─┘└─────────┘└─
doc ───────┘└────────────────────────────────────────┘┴ ┴ └─┘ └─┘ └─
txt ───────┘ ┴ ┴ └─┘ └─┘ └─
par ───────┘ ┴ ┴ └─┘ └─┘ └─
pid ─┘└────┘ ┴ ┴ └─┘ └─┘ ┴└
st ────────────────────────────────────────────────────────────────────────────────────────────
412
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
413 end
414
415 /-! ### Vector-valued functions `f : E → F` -/
416
417 /-- The mean value theorem on a convex set: if the derivative of a function is bounded by C, then
418 the function is C-Lipschitz -/
419 theorem convex.norm_image_sub_le_of_norm_deriv_le {f : E → F} {C : ℝ} {s : set E} {x y : E}
id ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ └─┘
typ ┴ ┴ ┴ └─┘ ┴ ┴
420 (hf : differentiable_on ℝ f s) (bound : ∀x∈s, ∥fderiv_within ℝ f s x∥ ≤ C)
id └───────────────┘ ┴ ┴ ┴ ┴ ┴ ┴└───────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴
src └───────────────┘ ┴ ┴└───────────┘ ┴ ┴ ┴
typ └───────────────┘ ┴ ┴ ┴ ┴ ┴ ┴└───────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴
doc └───────────────┘ └───────────┘
421 (hs : convex s) (xs : x ∈ s) (ys : y ∈ s) : ∥f y - f x∥ ≤ C * ∥y - x∥ :=
id └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
doc └────┘
422 begin
st └─────
423 /- By composition with t ↦ x + t • (y-x), we reduce to a statement for functions defined
st ───────────────────────────────────────────────────────────────────────────────────────────
424 on [0,1], for which it is proved in `norm_image_sub_le_of_norm_deriv_le_segment`.
st ────────────────────────────────────────────────────────────────────────────────────
425 We just have to check the differentiability of the composition and bounds on its derivative,
st ───────────────────────────────────────────────────────────────────────────────────────────────
426 which is straightforward but tedious for lack of automation. -/
st ──────────────────────────────────────────────────────────────────
427 have C0 : 0 ≤ C := le_trans (norm_nonneg _) (bound x xs),
id ┴ ┴ └──────┘ └─────────┘ └───┘ ┴ └┘
src └──────────┘┴┴ └──┘└──────┘┴ └─────────┘└──┘ ┴ ┴ ┴
typ └──────────┘┴┴┴└──┘└──────┘┴ └─────────┘└──┘ └───┘┴┴┴└┘┴
doc └──────────┘ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴
txt └──────────┘ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴
par └──────────┘ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴
pid └─────┘└───┘ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────┘└─
428 set g : ℝ → E := λ t, x + t • (y - x),
id ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ └──┘ └──┘ ┴┴┴ ┴┴┴ ┴┴┴ ┴
typ └──────┘ ┴ ┴┴└──┘ └──┘ ┴┴┴ ┴┴┴ ┴┴┴┴┴┴
doc └──────┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └──────┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └──────┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴┴└─┘ ┴ ┴ └─┘┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────┘└─
429 have Dg : ∀ t, has_deriv_at g (y-x) t,
id └──────────┘ ┴ ┴ ┴
src └────────┘ └┘ ┴└──────────┘┴ ┴ └┘
typ └────────┘ └┘ ┴└──────────┘┴┴┴ ┴ ┴└┘
doc └────────┘ └┘ ┴└──────────┘┴ ┴ └┘
txt └────────┘ └┘ ┴ ┴ ┴ └┘
par └────────┘ └┘ ┴ ┴ ┴ └┘
pid └─────┘└─┘ └┘ ┴ ┴ ┴ └┘
st ──────────────────────────────────────┘└─
430 { assume t,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───┘└──────┘└─
431 simpa only [one_smul] using ((has_deriv_at_id t).smul_const (y - x)).const_add x },
id └──────┘ └─────────────┘ ┴ ┴ ┴
src └──────────┘└──────┘└──────┘ └─────────────┘┴ └───────────┘ ┴ ┴ └───────────┘ ┴
typ └──────────┘└──────┘└──────┘ └─────────────┘┴┴└───────────┘ ┴┴ ┴ └───────────┘┴┴
doc └──────────┘ └──────┘ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴
txt └──────────┘ └──────┘ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴
par └──────────┘ └──────┘ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴
pid ┴└──┘└┘ ┴┴└────┘ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴
st ────────────────────────────────────────────────────────────────────────────────────┘└┘└
432 have segm : Icc 0 1 ⊆ g ⁻¹' s,
id └─┘ ┴ ┴ └─┘ ┴
src └──────────┘└─┘└───┘┴┴ ┴└─┘┴
typ └──────────┘└─┘└───┘┴┴┴┴└─┘┴┴
doc └──────────┘└─┘└───┘ ┴ ┴└─┘┴
txt └──────────┘ └───┘ ┴ ┴ ┴
par └──────────┘ └───┘ ┴ ┴ ┴
pid └───────┘└─┘ └───┘ ┴ ┴ ┴
st ──────────────────────────────┘└─
433 { rw [← image_subset_iff, ← segment_eq_image'],
id └──────────────┘ └───────────────┘
src └────┘└──────────────┘└──┘└───────────────┘┴
typ └────┘└──────────────┘└──┘└───────────────┘┴
doc └────┘└──────────────┘└──┘ ┴
txt └────┘ └──┘ ┴
par └────┘ └──┘ ┴
pid └──┘ └──┘ ┴
st ───┘└────────────────────┘└───────────────────┘└──
434 apply hs.segment_subset xs ys },
id └───────────────┘ └┘ └┘
src └────┘└───────────────┘┴ ┴ ┴
typ └────┘└───────────────┘┴└┘┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────────────────────┘└┘└
435 have : f x = f (g 0), by { simp only [g], rw [zero_smul, add_zero] },
id ┴ ┴ ┴ ┴ ┴ └───────┘ └──────┘
src └─────┘ ┴ ┴┴┴ ┴ └─┘ └─────────┘ ┴ └──┘└───────┘└┘└──────┘└┘
typ └─────┘ ┴┴┴┴┴┴┴ ┴└─┘ └─────────┘┴┴ └──┘└───────┘└┘└──────┘└┘
doc └─────┘ ┴ ┴ ┴ ┴ └─┘ └─────────┘ ┴ └──┘ └┘ └┘
txt └─────┘ ┴ ┴ ┴ ┴ └─┘ └─────────┘ ┴ └──┘ └┘ └┘
par └─────┘ ┴ ┴ ┴ ┴ └─┘ └─────────┘ ┴ └──┘ └┘ └┘
pid └───┘└┘ ┴ ┴ ┴ ┴ └─┘ ┴└──┘└┘ ┴ └┘ └┘ ┴┴
st ─────────────────────┘ ┴└────────────┘└─────────────┘└────────┘┴┴└┘└
436 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────┘└─
437 have : f y = f (g 1), by { simp only [g], rw [one_smul, add_sub_cancel'_right] },
id ┴ ┴ ┴ ┴ └──────┘ └───────────────────┘
src └─────┘ ┴ ┴ ┴ ┴ └─┘ └─────────┘ ┴ └──┘└──────┘└┘└───────────────────┘└┘
typ └─────┘ ┴┴┴ ┴┴┴ ┴└─┘ └─────────┘┴┴ └──┘└──────┘└┘└───────────────────┘└┘
doc └─────┘ ┴ ┴ ┴ ┴ └─┘ └─────────┘ ┴ └──┘ └┘ └┘
txt └─────┘ ┴ ┴ ┴ ┴ └─┘ └─────────┘ ┴ └──┘ └┘ └┘
par └─────┘ ┴ ┴ ┴ ┴ └─┘ └─────────┘ ┴ └──┘ └┘ └┘
pid └───┘└┘ ┴ ┴ ┴ ┴ └─┘ ┴└──┘└┘ ┴ └┘ └┘ ┴┴
st ─────────────────────┘ ┴└────────────┘└────────────┘└─────────────────────┘┴┴└┘└
438 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────┘└─
439 have D2: ∀ t ∈ Icc (0:ℝ) 1, has_deriv_within_at (f ∘ g)
id └─────────────────┘ ┴
src └───────┘ └───┘ ┴ └┘ └─┘ ┴└─────────────────┘┴ ┴┴┴ └─
typ └───────┘ └───┘ ┴ └┘ └─┘ ┴└─────────────────┘┴ ┴┴┴ └─
doc └───────┘ └───┘ ┴ └┘ └─┘ ┴└─────────────────┘┴ ┴ ┴ └─
txt └───────┘ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ └─
par └───────┘ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ └─
pid └─────┘└┘ └───┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ └─
st ──────────────────────────────────────────────────────────
440 ((fderiv_within ℝ f s (g t) : E → F) (y-x)) (Icc (0:ℝ) 1) t,
id └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src ───┘ └───────────┘┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └─┘ └─┘┴ └┘ └───┘
typ ───┘ └───────────┘┴ ┴┴┴┴┴ ┴┴ └──┘┴┴ ┴┴└┘ ┴ ┴└─┘ └─┘┴ └┘ └───┘
doc ───┘ └───────────┘┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └─┘ └─┘┴ └┘ └───┘
txt ───┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └─┘ ┴ └┘ └───┘
par ───┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └─┘ ┴ └┘ └───┘
pid ───┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └─┘ ┴ └┘ └───┘
st ──────────────────────────────────────────────────────────────┘└─
441 { intros t ht,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ───┘└─────────┘└─
442 exact (hf (g t) $ segm ht).has_fderiv_within_at.comp_has_deriv_within_at _
id └┘ ┴ └┘
src └────┘ ┴ ┴ └┘ ┴ ┴ └─────────────────────────────────────────────────
typ └────┘ └┘┴ ┴┴ └┘ ┴ ┴└┘└─────────────────────────────────────────────────
doc └────┘ ┴ ┴ └┘ ┴ ┴ └─────────────────────────────────────────────────
txt └────┘ ┴ ┴ └┘ ┴ ┴ └─────────────────────────────────────────────────
par └────┘ ┴ ┴ └┘ ┴ ┴ └─────────────────────────────────────────────────
pid ┴ ┴ ┴ └┘ ┴ ┴ └─────────────────────────────────────────────────
st ───────────────────────────────────────────────────────────────────────────────
443 (Dg t).has_deriv_within_at segm },
id └┘ ┴ └──┘
src ─────┘ ┴ └────────────────────┘ ┴
typ ─────┘ └┘┴┴└────────────────────┘└──┘┴
doc ─────┘ ┴ └────────────────────┘ ┴
txt ─────┘ ┴ └────────────────────┘ ┴
par ─────┘ ┴ └────────────────────┘ ┴
pid ─────┘ ┴ └────────────────────┘ ┴
st ─────────────────────────────────────┘└┘└
444 apply norm_image_sub_le_of_norm_deriv_le_segment_01' D2,
id └────────────────────────────────────────────┘ └┘
src └────┘└────────────────────────────────────────────┘┴
typ └────┘└────────────────────────────────────────────┘┴└┘
doc └────┘└────────────────────────────────────────────┘┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────────────────────────────────────────┘└─
445 assume t ht,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────┘└─
446 refine le_trans (le_op_norm _ _) (mul_le_mul_of_nonneg_right _ (norm_nonneg _)),
id └──────┘ └────────┘ └────────────────────────┘ └─────────┘
src └─────┘└──────┘┴ └────────┘└────┘ └────────────────────────┘└─┘ └─────────┘└──┘
typ └─────┘└──────┘┴ └────────┘└────┘ └────────────────────────┘└─┘ └─────────┘└──┘
doc └─────┘ ┴ └────────┘└────┘ └─┘ └──┘
txt └─────┘ ┴ └────┘ └─┘ └──┘
par └─────┘ ┴ └────┘ └─┘ └──┘
pid ┴ ┴ └────┘ └─┘ └──┘
st ────────────────────────────────────────────────────────────────────────────────┘└─
447 exact bound (g t) (segm $ Ico_subset_Icc_self ht)
id └───┘ ┴ ┴ └──┘ └─────────────────┘ └┘
src └────┘ ┴ ┴ └┘ ┴ ┴└─────────────────┘┴ └┘
typ └────┘└───┘┴ ┴┴┴└┘ └──┘┴ ┴└─────────────────┘┴└┘└┘
doc └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴┴
st ───────────────────────────────────────────────────┘
448 end
st └─┘
449
450 /-- If a function has zero Fréchet derivative at every point of a convex set,
451 then it is a constant on this set. -/
452 theorem convex.is_const_of_fderiv_within_eq_zero {s : set E} (hs : convex s)
id └─┘ ┴ └────┘ ┴
src └─┘ └────┘
typ └─┘ ┴ └────┘ ┴
doc └────┘
453 {f : E → F} (hf : differentiable_on ℝ f s) (hf' : ∀ x ∈ s, fderiv_within ℝ f s x = 0)
id ┴ ┴ └───────────────┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
src └───────────────┘ ┴ └───────────┘ ┴ ┴
typ ┴ ┴ └───────────────┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
doc └───────────────┘ └───────────┘
454 {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
455 f x = f y :=
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
456 have bound : ∀ x ∈ s, ∥fderiv_within ℝ f s x∥ ≤ 0,
id ┴ ┴ ┴└───────────┘ ┴ ┴ ┴ ┴┴ ┴
src ┴└───────────┘ ┴ ┴ ┴
typ ┴ ┴ ┴└───────────┘ ┴ ┴ ┴ ┴┴ ┴
doc └───────────┘
457 from λ x hx, by simp only [hf' x hx, _root_.norm_zero],
id ┴ └┘ └─┘ ┴ └┘ └──────────────┘
src └─────────┘ ┴ ┴ └┘└──────────────┘┴
typ ┴ └┘ └─────────┘└─┘┴┴┴└┘└┘└──────────────┘┴
doc └─────────┘ ┴ ┴ └┘ ┴
txt └─────────┘ ┴ ┴ └┘ ┴
par └─────────┘ ┴ ┴ └┘ ┴
pid ┴└──┘└┘ ┴ ┴ └┘ ┴
st └─────────────────────────────────────┘
458 by simpa only [(dist_eq_norm _ _).symm, zero_mul, dist_le_zero, eq_comm]
id └──────────┘ └──────┘ └──────────┘ └─────┘
src └──────────┘ └──────────┘└──────────┘└──────┘└┘└──────────┘└┘└─────┘└─
typ └──────────┘ └──────────┘└──────────┘└──────┘└┘└──────────┘└┘└─────┘└─
doc └──────────┘ └──────────┘ └┘ └┘ └─
txt └──────────┘ └──────────┘ └┘ └┘ └─
par └──────────┘ └──────────┘ └┘ └┘ └─
pid ┴└──┘└┘ └──────────┘ └┘ └┘ ┴└
st └──────────────────────────────────────────────────────────────────────
459 using hs.norm_image_sub_le_of_norm_deriv_le hf bound hx hy
id └───────────────────────────────────┘ └┘ └───┘ └┘ └┘
src ───────┘└───────────────────────────────────┘┴ ┴ ┴ ┴ └
typ ───────┘└───────────────────────────────────┘┴└┘┴└───┘┴└┘┴└┘└
doc ───────┘└───────────────────────────────────┘┴ ┴ ┴ ┴ └
txt ───────┘ ┴ ┴ ┴ ┴ └
par ───────┘ ┴ ┴ ┴ ┴ └
pid ─┘└────┘ ┴ ┴ ┴ ┴ └
st ─────────────────────────────────────────────────────────────
460
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
461 theorem is_const_of_fderiv_eq_zero {f : E → F} (hf : differentiable ℝ f)
id ┴ ┴ └────────────┘ ┴ ┴
src └────────────┘ ┴
typ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────┘
462 (hf' : ∀ x, fderiv ℝ f x = 0) (x y : E) :
id ┴ └────┘ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴ ┴
typ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
doc └────┘
463 f x = f y :=
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
464 convex_univ.is_const_of_fderiv_within_eq_zero hf.differentiable_on
id └─────────┘└────────────────────────────────┘ └┘└────────────────┘
src └─────────┘└────────────────────────────────┘ └────────────────┘
typ └─────────┘└────────────────────────────────┘ └┘└────────────────┘
doc └────────────────────────────────┘
465 (λ x _, by rw fderiv_within_univ; exact hf' x) trivial trivial
id ┴ ┴ └────────────────┘ └─┘ ┴ └─────┘ └─────┘
src └─┘└────────────────┘ └────┘ ┴ └─────┘ └─────┘
typ ┴ ┴ └─┘└────────────────┘ └────┘└─┘┴┴ └─────┘ └─────┘
doc └─┘ └────┘ ┴
txt └─┘ └────┘ ┴
par └─┘ └────┘ ┴
pid ┴ ┴ ┴
st └─────────────────────────────────┘
466
467 /-! ### Functions `[a, b] → ℝ`. -/
468
469 section interval
470
471 -- Declare all variables here to make sure they come in a correct order
472 variables (f f' : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hfc : continuous_on f (Icc a b))
id ┴ ┴ ┴ ┴ ┴ └───────────┘ └─┘
src ┴ ┴ ┴ ┴ └───────────┘ └─┘
typ ┴ ┴ ┴ ┴ ┴ └───────────┘ └─┘
doc └───────────┘ └─┘
473 (hff' : ∀ x ∈ Ioo a b, has_deriv_at f (f' x) x) (hfd : differentiable_on ℝ f (Ioo a b))
id ┴ └─┘ └──────────┘ ┴ ┴ └───────────────┘ ┴ └─┘
src └─┘ └──────────┘ └───────────────┘ ┴ └─┘
typ ┴ └─┘ └──────────┘ ┴ ┴ └───────────────┘ ┴ └─┘
doc └─┘ └──────────┘ └───────────────┘ └─┘
474 (g g' : ℝ → ℝ) (hgc : continuous_on g (Icc a b)) (hgg' : ∀ x ∈ Ioo a b, has_deriv_at g (g' x) x)
id ┴ ┴ └───────────┘ └─┘ ┴ └─┘ └──────────┘ ┴ ┴
src ┴ ┴ └───────────┘ └─┘ └─┘ └──────────┘
typ ┴ ┴ └───────────┘ └─┘ ┴ └─┘ └──────────┘ ┴ ┴
doc └───────────┘ └─┘ └─┘ └──────────┘
475 (hgd : differentiable_on ℝ g (Ioo a b))
id └───────────────┘ ┴ └─┘
src └───────────────┘ ┴ └─┘
typ └───────────────┘ ┴ └─┘
doc └───────────────┘ └─┘
476
477 include hab hfc hff' hgc hgg'
478
479 /-- Cauchy's Mean Value Theorem, `has_deriv_at` version. -/
480 lemma exists_ratio_has_deriv_at_eq_ratio_slope :
481 ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c :=
id ┴ ┴ └─┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
doc └─┘
482 begin
st └─────
483 let h := λ x, (g b - g a) * f x - (f b - f a) * g x,
id ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ └──┘ ┴ ┴┴┴ ┴ └┘┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
typ └───────┘ └──┘ ┴ ┴┴┴ ┴ └┘┴┴ ┴ ┴ ┴ ┴┴┴ ┴┴┴┴└┘ ┴┴┴
doc └───────┘ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
txt └───────┘ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
par └───────┘ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
pid └───┘┴└─┘ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
st ────────────────────────────────────────────────────┘└─
484 have hI : h a = h b,
id ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴┴┴ ┴
typ └────────┘ ┴┴┴┴┴┴┴┴
doc └────────┘ ┴ ┴ ┴ ┴
txt └────────┘ ┴ ┴ ┴ ┴
par └────────┘ ┴ ┴ ┴ ┴
pid └─────┘└─┘ ┴ ┴ ┴ ┴
st ────────────────────┘└─
485 { simp only [h], ring },
id ┴
src └─────────┘ ┴ └───┘
typ └─────────┘┴┴ └───┘
doc └─────────┘ ┴ └───┘
txt └─────────┘ ┴ └───┘
par └─────────┘ ┴ └───┘
pid ┴└──┘└┘ ┴ ┴
st ───┘└───────────┘└─────┘└┘└
486 let h' := λ x, (g b - g a) * f' x - (f b - f a) * g' x,
id ┴ └┘ ┴ ┴ ┴ └┘
src └────────┘ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
typ └────────┘ └──┘ ┴ ┴ ┴┴┴ └┘ ┴└┘┴ ┴ ┴ ┴┴┴ ┴┴┴┴└┘ ┴└┘┴
doc └────────┘ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
txt └────────┘ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
par └────────┘ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
pid └────┘┴└─┘ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
st ───────────────────────────────────────────────────────┘└─
487 have hhh' : ∀ x ∈ Ioo a b, has_deriv_at h (h' x) x,
id └─┘ ┴ ┴ └──────────┘ ┴ └┘
src └──────────┘ └───┘└─┘┴ ┴ ┴└──────────┘┴ ┴ ┴ └┘
typ └──────────┘ └───┘└─┘┴┴┴┴ ┴└──────────┘┴┴┴ └┘┴ └┘
doc └──────────┘ └───┘└─┘┴ ┴ ┴└──────────┘┴ ┴ ┴ └┘
txt └──────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par └──────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid └───────┘└─┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
st ───────────────────────────────────────────────────┘└─
488 from λ x hx, ((hff' x hx).const_mul (g b - g a)).sub ((hgg' x hx).const_mul (f b - f a)),
id └──┘ ┴ └──┘ ┴ ┴ ┴
src └───┘ └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ └┘
typ └───┘ └─────┘ └──┘┴ ┴ └──────────┘ ┴ ┴ ┴┴┴ └─────┘ └──┘┴ ┴ └──────────┘ ┴┴┴ ┴┴┴┴└┘
doc └───┘ └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ └┘
txt └───┘ └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ └┘
par └───┘ └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ └┘
pid └───┘ └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ └┘
st ───────────────────────────────────────────────────────────────────────────────────────────┘└─
489 have hhc : continuous_on h (Icc a b),
id └───────────┘ ┴ └─┘ ┴ ┴
src └─────────┘└───────────┘┴ ┴ └─┘┴ ┴ ┴
typ └─────────┘└───────────┘┴┴┴ └─┘┴┴┴┴┴
doc └─────────┘└───────────┘┴ ┴ └─┘┴ ┴ ┴
txt └─────────┘ ┴ ┴ ┴ ┴ ┴
par └─────────┘ ┴ ┴ ┴ ┴ ┴
pid └──────┘└─┘ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────┘└─
490 from (continuous_on_const.mul hfc).sub (continuous_on_const.mul hgc),
id └─┘ └─────────────────────┘ └─┘
src └───┘ ┴ └────┘ └─────────────────────┘┴ ┴
typ └───┘ ┴└─┘└────┘ └─────────────────────┘┴└─┘┴
doc └───┘ ┴ └────┘ ┴ ┴
txt └───┘ ┴ └────┘ ┴ ┴
par └───┘ ┴ └────┘ ┴ ┴
pid └───┘ ┴ └────┘ ┴ ┴
st ───────────────────────────────────────────────────────────────────────┘└─
491 rcases exists_has_deriv_at_eq_zero h h' hab hhc hI hhh' with ⟨c, cmem, hc⟩,
id └─────────────────────────┘ ┴ └┘ └─┘ └─┘ └┘ └──┘
src └─────┘└─────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
typ └─────┘└─────────────────────────┘┴┴┴└┘┴└─┘┴└─┘┴└┘┴└──┘└─────────────────┘
doc └─────┘└─────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘
st ───────────────────────────────────────────────────────────────────────────┘└─
492 exact ⟨c, cmem, sub_eq_zero.1 hc⟩
id ┴ └──┘ └─────────┘ └┘
src └────┘ └┘ └┘└─────────┘└─┘ └┘
typ └────┘ ┴└┘└──┘└┘└─────────┘└─┘└┘└┘
doc └────┘ └┘ └┘ └─┘ └┘
txt └────┘ └┘ └┘ └─┘ └┘
par └────┘ └┘ └┘ └─┘ └┘
pid ┴ └┘ └┘ └─┘ ┴┴
st ───────────────────────────────────┘
493 end
st └─┘
494
495 omit hgc hgg'
496
497 /-- Lagrange's Mean Value Theorem, `has_deriv_at` version -/
498 lemma exists_has_deriv_at_eq_slope : ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a) :=
id ┴ ┴ └─┘ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
499 begin
st └─────
500 rcases exists_ratio_has_deriv_at_eq_ratio_slope f f' hab hfc hff'
id └──────────────────────────────────────┘ ┴ └┘ └─┘ └─┘ └──┘
src └─────┘└──────────────────────────────────────┘┴ ┴ ┴ ┴ ┴ └
typ └─────┘└──────────────────────────────────────┘┴┴┴└┘┴└─┘┴└─┘┴└──┘└
doc └─────┘└──────────────────────────────────────┘┴ ┴ ┴ ┴ ┴ └
txt └─────┘ ┴ ┴ ┴ ┴ ┴ └
par └─────┘ ┴ ┴ ┴ ┴ ┴ └
pid ┴ ┴ ┴ ┴ ┴ ┴ └
st ────────────────────────────────────────────────────────────────────
501 id 1 continuous_id.continuous_on (λ x hx, has_deriv_at_id x) with ⟨c, cmem, hc⟩,
id └┘ └─────────────────────────┘ └─────────────┘
src ───┘└┘└─┘└─────────────────────────┘┴ └─────┘└─────────────┘┴ └──────────────────┘
typ ───┘└┘└─┘└─────────────────────────┘┴ └─────┘└─────────────┘┴ └──────────────────┘
doc ───┘ └─┘ ┴ └─────┘ ┴ └──────────────────┘
txt ───┘ └─┘ ┴ └─────┘ ┴ └──────────────────┘
par ───┘ └─┘ ┴ └─────┘ ┴ └──────────────────┘
pid ───┘ └─┘ ┴ └─────┘ ┴ └──────────────────┘
st ──────────────────────────────────────────────────────────────────────────────────┘└─
502 use [c, cmem],
id ┴ └──┘
src └───┘ └┘ ┴
typ └───┘┴└┘└──┘┴
doc └───┘ └┘ ┴
txt └───┘ └┘ ┴
par └───┘ └┘ ┴
pid └┘ └┘ ┴
st ──────────────┘└─
503 simp only [_root_.id, pi.one_apply, mul_one] at hc,
id └───────┘ └──────────┘ └─────┘
src └─────────┘└───────┘└┘└──────────┘└┘└─────┘└─────┘
typ └─────────┘└───────┘└┘└──────────┘└┘└─────┘└─────┘
doc └─────────┘ └┘ └┘ └─────┘
txt └─────────┘ └┘ └┘ └─────┘
par └─────────┘ └┘ └┘ └─────┘
pid ┴└──┘└┘ └┘ └┘ ┴┴└───┘
st ───────────────────────────────────────────────────┘└─
504 rw [← hc, mul_div_cancel_left],
id └┘ └─────────────────┘
src └────┘ └┘└─────────────────┘┴
typ └────┘└┘└┘└─────────────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid └──┘ └┘ ┴
st ─────────┘└───────────────────┘└──
505 exact ne_of_gt (sub_pos.2 hab)
id └──────┘ └─────┘ └─┘
src └────┘└──────┘┴ └─────┘└─┘ └┘
typ └────┘└──────┘┴ └─────┘└─┘└─┘└┘
doc └────┘ ┴ └─┘ └┘
txt └────┘ ┴ └─┘ └┘
par └────┘ ┴ └─┘ └┘
pid ┴ ┴ └─┘ ┴┴
st ────────────────────────────────┘
506 end
st └─┘
507
508 omit hff'
509
510 /-- Cauchy's Mean Value Theorem, `deriv` version. -/
511 lemma exists_ratio_deriv_eq_ratio_slope :
512 ∃ c ∈ Ioo a b, (g b - g a) * (deriv f c) = (f b - f a) * (deriv g c) :=
id ┴ ┴ └─┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘
typ ┴ ┴ └─┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
doc └─┘ └───┘ └───┘
513 exists_ratio_has_deriv_at_eq_ratio_slope f (deriv f) hab hfc
id └──────────────────────────────────────┘ ┴ └───┘ ┴ └─┘ └─┘
src └──────────────────────────────────────┘ └───┘
typ └──────────────────────────────────────┘ ┴ └───┘ ┴ └─┘ └─┘
doc └──────────────────────────────────────┘ └───┘
514 (λ x hx, ((hfd x hx).differentiable_at $ mem_nhds_sets is_open_Ioo hx).has_deriv_at)
id ┴ └┘ └─┘ ┴ └┘ └───────────────┘ └───────────┘ └─────────┘ └┘ └──────────┘
src └───────────────┘ └───────────┘ └─────────┘ └──────────┘
typ ┴ └┘ └─┘ ┴ └┘ └───────────────┘ └───────────┘ └─────────┘ └┘ └──────────┘
515 g (deriv g) hgc (λ x hx, ((hgd x hx).differentiable_at $ mem_nhds_sets is_open_Ioo hx).has_deriv_at)
id ┴ └───┘ ┴ └─┘ ┴ └┘ └─┘ ┴ └┘ └───────────────┘ └───────────┘ └─────────┘ └┘ └──────────┘
src └───┘ └───────────────┘ └───────────┘ └─────────┘ └──────────┘
typ ┴ └───┘ ┴ └─┘ ┴ └┘ └─┘ ┴ └┘ └───────────────┘ └───────────┘ └─────────┘ └┘ └──────────┘
doc └───┘
516
517 /-- Lagrange's Mean Value Theorem, `deriv` version. -/
518 lemma exists_deriv_eq_slope : ∃ c ∈ Ioo a b, deriv f c = (f b - f a) / (b - a) :=
id ┴ ┴ └─┘ ┴ ┴┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘ └───┘
519 exists_has_deriv_at_eq_slope f (deriv f) hab hfc
id └──────────────────────────┘ ┴ └───┘ ┴ └─┘ └─┘
src └──────────────────────────┘ └───┘
typ └──────────────────────────┘ ┴ └───┘ ┴ └─┘ └─┘
doc └──────────────────────────┘ └───┘
520 (λ x hx, ((hfd x hx).differentiable_at $ mem_nhds_sets is_open_Ioo hx).has_deriv_at)
id ┴ └┘ └─┘ ┴ └┘ └───────────────┘ └───────────┘ └─────────┘ └┘ └──────────┘
src └───────────────┘ └───────────┘ └─────────┘ └──────────┘
typ ┴ └┘ └─┘ ┴ └┘ └───────────────┘ └───────────┘ └─────────┘ └┘ └──────────┘
521
522 end interval
523
524 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
525 of the real line. If `f` is differentiable on the interior of `D` and `C < f'`, then
526 `f` grows faster than `C * x` on `D`, i.e., `C * (y - x) < f y - f x` whenever `x, y ∈ D`,
527 `x < y`. -/
528 theorem convex.mul_sub_lt_image_sub_of_lt_deriv {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id └─┘ ┴ └────┘ ┴ ┴ ┴
src └─┘ ┴ └────┘ ┴ ┴
typ └─┘ ┴ └────┘ ┴ ┴ ┴
doc └────┘
529 (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
src └───────────┘ └───────────────┘ ┴ └──────┘
typ └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
doc └───────────┘ └───────────────┘ └──────┘
530 {C} (hf'_gt : ∀ x ∈ interior D, C < deriv f x) :
id ┴ └──────┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └──────┘ ┴ └───┘
typ ┴ └──────┘ ┴ ┴ ┴ └───┘ ┴ ┴
doc └──────┘ └───┘
531 ∀ x y ∈ D, x < y → C * (y - x) < f y - f x :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
532 begin
st └─────
533 assume x y hx hy hxy,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └──────────────────┘
st ─────────────────────┘└─
534 have hxyD : Icc x y ⊆ D, from convex_real_iff.1 hD hx hy,
id └─┘ ┴ ┴ ┴ ┴ └─────────────┘ └┘ └┘ └┘
src └──────────┘└─┘┴ ┴ ┴┴┴ └───┘└─────────────┘└─┘ ┴ ┴
typ └──────────┘└─┘┴┴┴┴┴┴┴┴ └───┘└─────────────┘└─┘└┘┴└┘┴└┘
doc └──────────┘└─┘┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴
txt └──────────┘ ┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴
par └──────────┘ ┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴
pid └───────┘└─┘ ┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴
st ────────────────────────┘└───────────────────────────────┘└─
535 have hxyD' : Ioo x y ⊆ interior D,
id └─┘ ┴ ┴ └──────┘ ┴
src └───────────┘└─┘┴ ┴ ┴ ┴└──────┘┴
typ └───────────┘└─┘┴┴┴┴┴ ┴└──────┘┴┴
doc └───────────┘└─┘┴ ┴ ┴ ┴└──────┘┴
txt └───────────┘ ┴ ┴ ┴ ┴ ┴
par └───────────┘ ┴ ┴ ┴ ┴ ┴
pid └────────┘└─┘ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────┘└─
536 from subset_sUnion_of_mem ⟨is_open_Ioo, subset.trans Ioo_subset_Icc_self hxyD⟩,
id └──────────────────┘ └─────────┘ └──────────┘ └─────────────────┘ └──┘
src └───┘└──────────────────┘┴ └─────────┘└┘└──────────┘┴└─────────────────┘┴ ┴
typ └───┘└──────────────────┘┴ └─────────┘└┘└──────────┘┴└─────────────────┘┴└──┘┴
doc └───┘ ┴ └┘ ┴ ┴ ┴
txt └───┘ ┴ └┘ ┴ ┴ ┴
par └───┘ ┴ └┘ ┴ ┴ ┴
pid └───┘ ┴ └┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────────┘└─
537 obtain ⟨a, a_mem, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x),
id ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────────────────┘┴└───┘└─┘┴ ┴ ┴┴└───┘┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ └┘┴┴ ┴ ┴ ┴
typ └──────────────────────┘┴└───┘└─┘┴ ┴ ┴┴└───┘┴ ┴ ┴┴┴ ┴ ┴┴┴┴┴ └┘┴┴ ┴┴ ┴┴┴
doc └──────────────────────┘ └───┘└─┘┴ ┴ ┴└───┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
txt └──────────────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
par └──────────────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
pid └────────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────┘└─
538 from exists_deriv_eq_slope f hxy (hf.mono hxyD) (hf'.mono hxyD'),
id └───────────────────┘ ┴ └─┘ └─────┘ └──┘ └──────┘ └───┘
src └───┘└───────────────────┘┴ ┴ ┴ └─────┘┴ └┘ └──────┘┴ ┴
typ └───┘└───────────────────┘┴┴┴└─┘┴ └─────┘┴└──┘└┘ └──────┘┴└───┘┴
doc └───┘└───────────────────┘┴ ┴ ┴ ┴ └┘ ┴ ┴
txt └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
par └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
pid └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
st ───────────────────────────────────────────────────────────────────┘└─
539 have : C < (f y - f x) / (y - x), by { rw [← ha], exact hf'_gt _ (hxyD' a_mem) },
id ┴ ┴ ┴ ┴ ┴ └┘ └────┘ └───┘ └───┘
src └─────┘ ┴┴┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────┘ ┴ └────┘ └─┘ ┴ └┘
typ └─────┘┴┴┴┴ ┴ ┴ ┴┴┴ └┘ ┴ ┴┴ ┴┴┴ └────┘└┘┴ └────┘└────┘└─┘ └───┘┴└───┘└┘
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────┘ ┴ └────┘ └─┘ ┴ └┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────┘ ┴ └────┘ └─┘ ┴ └┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────┘ ┴ └────┘ └─┘ ┴ └┘
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴┴
st ─────────────────────────────────┘ ┴└───────┘└──────────────────────────────┘└┘└
540 exact (lt_div_iff (sub_pos.2 hxy)).1 this
id └────────┘ └─────┘ └─┘ └──┘
src └────┘ └────────┘┴ └─────┘└─┘ └───┘ ┴
typ └────┘ └────────┘┴ └─────┘└─┘└─┘└───┘└──┘┴
doc └────┘ ┴ └─┘ └───┘ ┴
txt └────┘ ┴ └─┘ └───┘ ┴
par └────┘ ┴ └─┘ └───┘ ┴
pid ┴ ┴ └─┘ └───┘ ┴
st ───────────────────────────────────────────┘
541 end
st └─┘
542
543 /-- Let `f : ℝ → ℝ` be a differentiable function. If `C < f'`, then `f` grows faster than
544 `C * x`, i.e., `C * (y - x) < f y - f x` whenever `x < y`. -/
545 theorem mul_sub_lt_image_sub_of_lt_deriv {f : ℝ → ℝ} (hf : differentiable ℝ f)
id ┴ ┴ └────────────┘ ┴ ┴
src ┴ ┴ └────────────┘ ┴
typ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────┘
546 {C} (hf'_gt : ∀ x, C < deriv f x) ⦃x y⦄ (hxy : x < y) :
id ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴
typ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └───┘
547 C * (y - x) < f y - f x :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
548 convex_univ.mul_sub_lt_image_sub_of_lt_deriv hf.continuous.continuous_on hf.differentiable_on
id └─────────┘└───────────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
src └─────────┘└───────────────────────────────┘ └─────────┘└────────────┘ └────────────────┘
typ └─────────┘└───────────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
doc └───────────────────────────────┘
549 (λ x _, hf'_gt x) x y trivial trivial hxy
id ┴ ┴ └────┘ ┴ ┴ ┴ └─────┘ └─────┘ └─┘
src └─────┘ └─────┘
typ ┴ ┴ └────┘ ┴ ┴ ┴ └─────┘ └─────┘ └─┘
550
551 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
552 of the real line. If `f` is differentiable on the interior of `D` and `C ≤ f'`, then
553 `f` grows at least as fast as `C * x` on `D`, i.e., `C * (y - x) ≤ f y - f x` whenever `x, y ∈ D`,
554 `x ≤ y`. -/
555 theorem convex.mul_sub_le_image_sub_of_le_deriv {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id └─┘ ┴ └────┘ ┴ ┴ ┴
src └─┘ ┴ └────┘ ┴ ┴
typ └─┘ ┴ └────┘ ┴ ┴ ┴
doc └────┘
556 (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
src └───────────┘ └───────────────┘ ┴ └──────┘
typ └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
doc └───────────┘ └───────────────┘ └──────┘
557 {C} (hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x) :
id ┴ └──────┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └──────┘ ┴ └───┘
typ ┴ └──────┘ ┴ ┴ ┴ └───┘ ┴ ┴
doc └──────┘ └───┘
558 ∀ x y ∈ D, x ≤ y → C * (y - x) ≤ f y - f x :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
559 begin
st └─────
560 assume x y hx hy hxy,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └──────────────────┘
st ─────────────────────┘└─
561 cases eq_or_lt_of_le hxy with hxy' hxy', by rw [hxy', sub_self, sub_self, mul_zero],
id └────────────┘ └─┘ └──┘ └──────┘ └──────┘ └──────┘
src └────┘└────────────┘┴ └─────────────┘ └──┘ └┘└──────┘└┘└──────┘└┘└──────┘┴
typ └────┘└────────────┘┴└─┘└─────────────┘ └──┘└──┘└┘└──────┘└┘└──────┘└┘└──────┘┴
doc └────┘ ┴ └─────────────┘ └──┘ └┘ └┘ └┘ ┴
txt └────┘ ┴ └─────────────┘ └──┘ └┘ └┘ └┘ ┴
par └────┘ ┴ └─────────────┘ └──┘ └┘ └┘ └┘ ┴
pid ┴ ┴ └─────────────┘ └┘ └┘ └┘ └┘ ┴
st ────────────────────────────────────────┘ └──┘└────────┘└────────┘└────────┘┴└─
562 have hxyD : Icc x y ⊆ D, from convex_real_iff.1 hD hx hy,
id └─┘ ┴ ┴ ┴ ┴ └─────────────┘ └┘ └┘ └┘
src └──────────┘└─┘┴ ┴ ┴┴┴ └───┘└─────────────┘└─┘ ┴ ┴
typ └──────────┘└─┘┴┴┴┴┴┴┴┴ └───┘└─────────────┘└─┘└┘┴└┘┴└┘
doc └──────────┘└─┘┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴
txt └──────────┘ ┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴
par └──────────┘ ┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴
pid └───────┘└─┘ ┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴
st ────────────────────────┘└───────────────────────────────┘└─
563 have hxyD' : Ioo x y ⊆ interior D,
id └─┘ ┴ ┴ └──────┘ ┴
src └───────────┘└─┘┴ ┴ ┴ ┴└──────┘┴
typ └───────────┘└─┘┴┴┴┴┴ ┴└──────┘┴┴
doc └───────────┘└─┘┴ ┴ ┴ ┴└──────┘┴
txt └───────────┘ ┴ ┴ ┴ ┴ ┴
par └───────────┘ ┴ ┴ ┴ ┴ ┴
pid └────────┘└─┘ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────┘└─
564 from subset_sUnion_of_mem ⟨is_open_Ioo, subset.trans Ioo_subset_Icc_self hxyD⟩,
id └──────────────────┘ └─────────┘ └──────────┘ └─────────────────┘ └──┘
src └───┘└──────────────────┘┴ └─────────┘└┘└──────────┘┴└─────────────────┘┴ ┴
typ └───┘└──────────────────┘┴ └─────────┘└┘└──────────┘┴└─────────────────┘┴└──┘┴
doc └───┘ ┴ └┘ ┴ ┴ ┴
txt └───┘ ┴ └┘ ┴ ┴ ┴
par └───┘ ┴ └┘ ┴ ┴ ┴
pid └───┘ ┴ └┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────────┘└─
565 obtain ⟨a, a_mem, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x),
id ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────────────────┘┴└───┘└─┘┴ ┴ ┴┴└───┘┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ └┘┴┴ ┴ ┴ ┴
typ └──────────────────────┘┴└───┘└─┘┴ ┴ ┴┴└───┘┴ ┴ ┴┴┴ ┴ ┴┴┴┴┴ └┘┴┴ ┴┴ ┴┴┴
doc └──────────────────────┘ └───┘└─┘┴ ┴ ┴└───┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
txt └──────────────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
par └──────────────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
pid └────────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────┘└─
566 from exists_deriv_eq_slope f hxy' (hf.mono hxyD) (hf'.mono hxyD'),
id └───────────────────┘ ┴ └──┘ └─────┘ └──┘ └──────┘ └───┘
src └───┘└───────────────────┘┴ ┴ ┴ └─────┘┴ └┘ └──────┘┴ ┴
typ └───┘└───────────────────┘┴┴┴└──┘┴ └─────┘┴└──┘└┘ └──────┘┴└───┘┴
doc └───┘└───────────────────┘┴ ┴ ┴ ┴ └┘ ┴ ┴
txt └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
par └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
pid └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
st ────────────────────────────────────────────────────────────────────┘└─
567 have : C ≤ (f y - f x) / (y - x), by { rw [← ha], exact hf'_ge _ (hxyD' a_mem) },
id ┴ ┴ ┴ ┴ ┴ └┘ └────┘ └───┘ └───┘
src └─────┘ ┴┴┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────┘ ┴ └────┘ └─┘ ┴ └┘
typ └─────┘┴┴┴┴ ┴ ┴ ┴┴┴ └┘ ┴ ┴┴ ┴┴┴ └────┘└┘┴ └────┘└────┘└─┘ └───┘┴└───┘└┘
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────┘ ┴ └────┘ └─┘ ┴ └┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────┘ ┴ └────┘ └─┘ ┴ └┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────┘ ┴ └────┘ └─┘ ┴ └┘
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴┴
st ─────────────────────────────────┘ ┴└───────┘└──────────────────────────────┘└┘└
568 exact (le_div_iff (sub_pos.2 hxy')).1 this
id └────────┘ └─────┘ └──┘ └──┘
src └────┘ └────────┘┴ └─────┘└─┘ └───┘ ┴
typ └────┘ └────────┘┴ └─────┘└─┘└──┘└───┘└──┘┴
doc └────┘ ┴ └─┘ └───┘ ┴
txt └────┘ ┴ └─┘ └───┘ ┴
par └────┘ ┴ └─┘ └───┘ ┴
pid ┴ ┴ └─┘ └───┘ ┴
st ────────────────────────────────────────────┘
569 end
st └─┘
570
571 /-- Let `f : ℝ → ℝ` be a differentiable function. If `C ≤ f'`, then `f` grows at least as fast
572 as `C * x`, i.e., `C * (y - x) ≤ f y - f x` whenever `x ≤ y`. -/
573 theorem mul_sub_le_image_sub_of_le_deriv {f : ℝ → ℝ} (hf : differentiable ℝ f)
id ┴ ┴ └────────────┘ ┴ ┴
src ┴ ┴ └────────────┘ ┴
typ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────┘
574 {C} (hf'_ge : ∀ x, C ≤ deriv f x) ⦃x y⦄ (hxy : x ≤ y) :
id ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴
typ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └───┘
575 C * (y - x) ≤ f y - f x :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
576 convex_univ.mul_sub_le_image_sub_of_le_deriv hf.continuous.continuous_on hf.differentiable_on
id └─────────┘└───────────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
src └─────────┘└───────────────────────────────┘ └─────────┘└────────────┘ └────────────────┘
typ └─────────┘└───────────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
doc └───────────────────────────────┘
577 (λ x _, hf'_ge x) x y trivial trivial hxy
id ┴ ┴ └────┘ ┴ ┴ ┴ └─────┘ └─────┘ └─┘
src └─────┘ └─────┘
typ ┴ ┴ └────┘ ┴ ┴ ┴ └─────┘ └─────┘ └─┘
578
579 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
580 of the real line. If `f` is differentiable on the interior of `D` and `f' < C`, then
581 `f` grows slower than `C * x` on `D`, i.e., `f y - f x < C * (y - x)` whenever `x, y ∈ D`,
582 `x < y`. -/
583 theorem convex.image_sub_lt_mul_sub_of_deriv_lt {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id └─┘ ┴ └────┘ ┴ ┴ ┴
src └─┘ ┴ └────┘ ┴ ┴
typ └─┘ ┴ └────┘ ┴ ┴ ┴
doc └────┘
584 (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
src └───────────┘ └───────────────┘ ┴ └──────┘
typ └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
doc └───────────┘ └───────────────┘ └──────┘
585 {C} (lt_hf' : ∀ x ∈ interior D, deriv f x < C) :
id ┴ └──────┘ ┴ └───┘ ┴ ┴ ┴ ┴
src └──────┘ └───┘ ┴
typ ┴ └──────┘ ┴ └───┘ ┴ ┴ ┴ ┴
doc └──────┘ └───┘
586 ∀ x y ∈ D, x < y → f y - f x < C * (y - x) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
587 begin
st └─────
588 assume x y hx hy hxy,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └──────────────────┘
st ─────────────────────┘└─
589 have hf'_gt : ∀ x ∈ interior D, -C < deriv (λ y, -f y) x,
id └──────┘ ┴ ┴┴ ┴ └───┘ ┴
src └────────────┘ └───┘└──────┘┴ ┴┴ ┴┴┴└───┘┴ └──┘ ┴ └┘
typ └────────────┘ └───┘└──────┘┴┴ ┴┴┴┴┴┴└───┘┴ └──┘ ┴┴ └┘
doc └────────────┘ └───┘└──────┘┴ ┴ ┴ ┴└───┘┴ └──┘ ┴ └┘
txt └────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘
par └────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘
pid └─────────┘└─┘ └───┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘
st ─────────────────────────────────────────────────────────┘└─
590 { assume x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───┘└─────────┘└─
591 rw [deriv_neg, neg_lt_neg_iff],
id └───────┘ └────────────┘
src └──┘└───────┘└┘└────────────┘┴
typ └──┘└───────┘└┘└────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ────────────────┘└──────────────┘└──
592 exact lt_hf' x hx },
id └────┘ ┴ └┘
src └────┘ ┴ ┴ ┴
typ └────┘└────┘┴┴┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────────┘└┘└
593 simpa [-neg_lt_neg_iff]
src └───────────────────────
typ └───────────────────────
doc └───────────────────────
txt └───────────────────────
par └───────────────────────
pid ┴└───────────────┘└
st ──────────────────────────
594 using neg_lt_neg (hD.mul_sub_lt_image_sub_of_lt_deriv hf.neg hf'.neg hf'_gt x y hx hy hxy)
id └────────┘ └─────────────────────────────────┘ └────┘ └─────┘ └────┘ ┴ ┴ └┘ └┘ └─┘
src ─────────┘└────────┘┴ └─────────────────────────────────┘┴└────┘┴└─────┘┴ ┴ ┴ ┴ ┴ ┴ └┘
typ ─────────┘└────────┘┴ └─────────────────────────────────┘┴└────┘┴└─────┘┴└────┘┴┴┴┴┴└┘┴└┘┴└─┘└┘
doc ─────────┘ ┴ └─────────────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
txt ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid ───┘└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
st ──────────────────────────────────────────────────────────────────────────────────────────────┘
595 end
st └─┘
596
597 /-- Let `f : ℝ → ℝ` be a differentiable function. If `f' < C`, then `f` grows slower than
598 `C * x` on `D`, i.e., `f y - f x < C * (y - x)` whenever `x < y`. -/
599 theorem image_sub_lt_mul_sub_of_deriv_lt {f : ℝ → ℝ} (hf : differentiable ℝ f)
id ┴ ┴ └────────────┘ ┴ ┴
src ┴ ┴ └────────────┘ ┴
typ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────┘
600 {C} (lt_hf' : ∀ x, deriv f x < C) ⦃x y⦄ (hxy : x < y) :
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘
601 f y - f x < C * (y - x) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
602 convex_univ.image_sub_lt_mul_sub_of_deriv_lt hf.continuous.continuous_on hf.differentiable_on
id └─────────┘└───────────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
src └─────────┘└───────────────────────────────┘ └─────────┘└────────────┘ └────────────────┘
typ └─────────┘└───────────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
doc └───────────────────────────────┘
603 (λ x _, lt_hf' x) x y trivial trivial hxy
id ┴ ┴ └────┘ ┴ ┴ ┴ └─────┘ └─────┘ └─┘
src └─────┘ └─────┘
typ ┴ ┴ └────┘ ┴ ┴ ┴ └─────┘ └─────┘ └─┘
604
605 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
606 of the real line. If `f` is differentiable on the interior of `D` and `f' ≤ C`, then
607 `f` grows at most as fast as `C * x` on `D`, i.e., `f y - f x ≤ C * (y - x)` whenever `x, y ∈ D`,
608 `x ≤ y`. -/
609 theorem convex.image_sub_le_mul_sub_of_deriv_le {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id └─┘ ┴ └────┘ ┴ ┴ ┴
src └─┘ ┴ └────┘ ┴ ┴
typ └─┘ ┴ └────┘ ┴ ┴ ┴
doc └────┘
610 (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
src └───────────┘ └───────────────┘ ┴ └──────┘
typ └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
doc └───────────┘ └───────────────┘ └──────┘
611 {C} (le_hf' : ∀ x ∈ interior D, deriv f x ≤ C) :
id ┴ └──────┘ ┴ └───┘ ┴ ┴ ┴ ┴
src └──────┘ └───┘ ┴
typ ┴ └──────┘ ┴ └───┘ ┴ ┴ ┴ ┴
doc └──────┘ └───┘
612 ∀ x y ∈ D, x ≤ y → f y - f x ≤ C * (y - x) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
613 begin
st └─────
614 assume x y hx hy hxy,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └──────────────────┘
st ─────────────────────┘└─
615 have hf'_ge : ∀ x ∈ interior D, -C ≤ deriv (λ y, -f y) x,
id └──────┘ ┴ ┴┴ ┴ └───┘ ┴
src └────────────┘ └───┘└──────┘┴ ┴┴ ┴┴┴└───┘┴ └──┘ ┴ └┘
typ └────────────┘ └───┘└──────┘┴┴ ┴┴┴┴┴┴└───┘┴ └──┘ ┴┴ └┘
doc └────────────┘ └───┘└──────┘┴ ┴ ┴ ┴└───┘┴ └──┘ ┴ └┘
txt └────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘
par └────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘
pid └─────────┘└─┘ └───┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘
st ─────────────────────────────────────────────────────────┘└─
616 { assume x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───┘└─────────┘└─
617 rw [deriv_neg, neg_le_neg_iff],
id └───────┘ └────────────┘
src └──┘└───────┘└┘└────────────┘┴
typ └──┘└───────┘└┘└────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ────────────────┘└──────────────┘└──
618 exact le_hf' x hx },
id └────┘ ┴ └┘
src └────┘ ┴ ┴ ┴
typ └────┘└────┘┴┴┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────────┘└┘└
619 simpa [-neg_le_neg_iff]
src └───────────────────────
typ └───────────────────────
doc └───────────────────────
txt └───────────────────────
par └───────────────────────
pid ┴└───────────────┘└
st ──────────────────────────
620 using neg_le_neg (hD.mul_sub_le_image_sub_of_le_deriv hf.neg hf'.neg hf'_ge x y hx hy hxy)
id └────────┘ └─────────────────────────────────┘ └────┘ └─────┘ └────┘ ┴ ┴ └┘ └┘ └─┘
src ─────────┘└────────┘┴ └─────────────────────────────────┘┴└────┘┴└─────┘┴ ┴ ┴ ┴ ┴ ┴ └┘
typ ─────────┘└────────┘┴ └─────────────────────────────────┘┴└────┘┴└─────┘┴└────┘┴┴┴┴┴└┘┴└┘┴└─┘└┘
doc ─────────┘ ┴ └─────────────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
txt ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid ───┘└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
st ──────────────────────────────────────────────────────────────────────────────────────────────┘
621 end
st └─┘
622
623 /-- Let `f : ℝ → ℝ` be a differentiable function. If `f' ≤ C`, then `f` grows at most as fast
624 as `C * x`, i.e., `f y - f x ≤ C * (y - x)` whenever `x ≤ y`. -/
625 theorem image_sub_le_mul_sub_of_deriv_le {f : ℝ → ℝ} (hf : differentiable ℝ f)
id ┴ ┴ └────────────┘ ┴ ┴
src ┴ ┴ └────────────┘ ┴
typ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────┘
626 {C} (le_hf' : ∀ x, deriv f x ≤ C) ⦃x y⦄ (hxy : x ≤ y) :
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘
627 f y - f x ≤ C * (y - x) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
628 convex_univ.image_sub_le_mul_sub_of_deriv_le hf.continuous.continuous_on hf.differentiable_on
id └─────────┘└───────────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
src └─────────┘└───────────────────────────────┘ └─────────┘└────────────┘ └────────────────┘
typ └─────────┘└───────────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
doc └───────────────────────────────┘
629 (λ x _, le_hf' x) x y trivial trivial hxy
id ┴ ┴ └────┘ ┴ ┴ ┴ └─────┘ └─────┘ └─┘
src └─────┘ └─────┘
typ ┴ ┴ └────┘ ┴ ┴ ┴ └─────┘ └─────┘ └─┘
630
631 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
632 of the real line. If `f` is differentiable on the interior of `D` and `f'` is positive, then
633 `f` is a strictly monotonically increasing function on `D`. -/
634 theorem convex.strict_mono_of_deriv_pos {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id └─┘ ┴ └────┘ ┴ ┴ ┴
src └─┘ ┴ └────┘ ┴ ┴
typ └─┘ ┴ └────┘ ┴ ┴ ┴
doc └────┘
635 (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
src └───────────┘ └───────────────┘ ┴ └──────┘
typ └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
doc └───────────┘ └───────────────┘ └──────┘
636 (hf'_pos : ∀ x ∈ interior D, 0 < deriv f x) :
id ┴ └──────┘ ┴ ┴ └───┘ ┴ ┴
src └──────┘ ┴ └───┘
typ ┴ └──────┘ ┴ ┴ └───┘ ┴ ┴
doc └──────┘ └───┘
637 ∀ x y ∈ D, x < y → f x < f y :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
638 by simpa only [zero_mul, sub_pos] using hD.mul_sub_lt_image_sub_of_lt_deriv hf hf' hf'_pos
id └──────┘ └─────┘ └─────────────────────────────────┘ └┘ └─┘ └─────┘
src └──────────┘└──────┘└┘└─────┘└──────┘└─────────────────────────────────┘┴ ┴ ┴ └
typ └──────────┘└──────┘└┘└─────┘└──────┘└─────────────────────────────────┘┴└┘┴└─┘┴└─────┘└
doc └──────────┘ └┘ └──────┘└─────────────────────────────────┘┴ ┴ ┴ └
txt └──────────┘ └┘ └──────┘ ┴ ┴ ┴ └
par └──────────┘ └┘ └──────┘ ┴ ┴ ┴ └
pid ┴└──┘└┘ └┘ ┴┴└────┘ ┴ ┴ ┴ └
st └────────────────────────────────────────────────────────────────────────────────────────
639
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
640 /-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is positive, then
641 `f` is a strictly monotonically increasing function. -/
642 theorem strict_mono_of_deriv_pos {f : ℝ → ℝ} (hf : differentiable ℝ f)
id ┴ ┴ └────────────┘ ┴ ┴
src ┴ ┴ └────────────┘ ┴
typ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────┘
643 (hf'_pos : ∀ x, 0 < deriv f x) :
id ┴ ┴ └───┘ ┴ ┴
src ┴ └───┘
typ ┴ ┴ └───┘ ┴ ┴
doc └───┘
644 strict_mono f :=
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
doc └─────────┘
645 λ x y hxy, convex_univ.strict_mono_of_deriv_pos hf.continuous.continuous_on hf.differentiable_on
id ┴ ┴ └─┘ └─────────┘└───────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
src └─────────┘└───────────────────────┘ └─────────┘└────────────┘ └────────────────┘
typ ┴ ┴ └─┘ └─────────┘└───────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
doc └───────────────────────┘
646 (λ x _, hf'_pos x) x y trivial trivial hxy
id ┴ ┴ └─────┘ ┴ ┴ ┴ └─────┘ └─────┘ └─┘
src └─────┘ └─────┘
typ ┴ ┴ └─────┘ ┴ ┴ ┴ └─────┘ └─────┘ └─┘
647
648 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
649 of the real line. If `f` is differentiable on the interior of `D` and `f'` is nonnegative, then
650 `f` is a monotonically increasing function on `D`. -/
651 theorem convex.mono_of_deriv_nonneg {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id └─┘ ┴ └────┘ ┴ ┴ ┴
src └─┘ ┴ └────┘ ┴ ┴
typ └─┘ ┴ └────┘ ┴ ┴ ┴
doc └────┘
652 (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
src └───────────┘ └───────────────┘ ┴ └──────┘
typ └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
doc └───────────┘ └───────────────┘ └──────┘
653 (hf'_nonneg : ∀ x ∈ interior D, 0 ≤ deriv f x) :
id ┴ └──────┘ ┴ ┴ └───┘ ┴ ┴
src └──────┘ ┴ └───┘
typ ┴ └──────┘ ┴ ┴ └───┘ ┴ ┴
doc └──────┘ └───┘
654 ∀ x y ∈ D, x ≤ y → f x ≤ f y :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
655 by simpa only [zero_mul, sub_nonneg] using hD.mul_sub_le_image_sub_of_le_deriv hf hf' hf'_nonneg
id └──────┘ └────────┘ └─────────────────────────────────┘ └┘ └─┘ └────────┘
src └──────────┘└──────┘└┘└────────┘└──────┘└─────────────────────────────────┘┴ ┴ ┴ └
typ └──────────┘└──────┘└┘└────────┘└──────┘└─────────────────────────────────┘┴└┘┴└─┘┴└────────┘└
doc └──────────┘ └┘ └──────┘└─────────────────────────────────┘┴ ┴ ┴ └
txt └──────────┘ └┘ └──────┘ ┴ ┴ ┴ └
par └──────────┘ └┘ └──────┘ ┴ ┴ ┴ └
pid ┴└──┘└┘ └┘ ┴┴└────┘ ┴ ┴ ┴ └
st └──────────────────────────────────────────────────────────────────────────────────────────────
656
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
657 /-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is nonnegative, then
658 `f` is a monotonically increasing function. -/
659 theorem mono_of_deriv_nonneg {f : ℝ → ℝ} (hf : differentiable ℝ f) (hf' : ∀ x, 0 ≤ deriv f x) :
id ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
src ┴ ┴ └────────────┘ ┴ ┴ └───┘
typ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
doc └────────────┘ └───┘
660 monotone f :=
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
doc └──────┘
661 λ x y hxy, convex_univ.mono_of_deriv_nonneg hf.continuous.continuous_on hf.differentiable_on
id ┴ ┴ └─┘ └─────────┘└───────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
src └─────────┘└───────────────────┘ └─────────┘└────────────┘ └────────────────┘
typ ┴ ┴ └─┘ └─────────┘└───────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
doc └───────────────────┘
662 (λ x _, hf' x) x y trivial trivial hxy
id ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ └─────┘ └─┘
src └─────┘ └─────┘
typ ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ └─────┘ └─┘
663
664 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
665 of the real line. If `f` is differentiable on the interior of `D` and `f'` is negative, then
666 `f` is a strictly monotonically decreasing function on `D`. -/
667 theorem convex.strict_antimono_of_deriv_neg {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id └─┘ ┴ └────┘ ┴ ┴ ┴
src └─┘ ┴ └────┘ ┴ ┴
typ └─┘ ┴ └────┘ ┴ ┴ ┴
doc └────┘
668 (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
src └───────────┘ └───────────────┘ ┴ └──────┘
typ └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
doc └───────────┘ └───────────────┘ └──────┘
669 (hf'_neg : ∀ x ∈ interior D, deriv f x < 0) :
id ┴ └──────┘ ┴ └───┘ ┴ ┴ ┴
src └──────┘ └───┘ ┴
typ ┴ └──────┘ ┴ └───┘ ┴ ┴ ┴
doc └──────┘ └───┘
670 ∀ x y ∈ D, x < y → f y < f x :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
671 by simpa only [zero_mul, sub_lt_zero] using hD.image_sub_lt_mul_sub_of_deriv_lt hf hf' hf'_neg
id └──────┘ └─────────┘ └─────────────────────────────────┘ └┘ └─┘ └─────┘
src └──────────┘└──────┘└┘└─────────┘└──────┘└─────────────────────────────────┘┴ ┴ ┴ └
typ └──────────┘└──────┘└┘└─────────┘└──────┘└─────────────────────────────────┘┴└┘┴└─┘┴└─────┘└
doc └──────────┘ └┘ └──────┘└─────────────────────────────────┘┴ ┴ ┴ └
txt └──────────┘ └┘ └──────┘ ┴ ┴ ┴ └
par └──────────┘ └┘ └──────┘ ┴ ┴ ┴ └
pid ┴└──┘└┘ └┘ ┴┴└────┘ ┴ ┴ ┴ └
st └────────────────────────────────────────────────────────────────────────────────────────────
672
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
673 /-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is negative, then
674 `f` is a strictly monotonically decreasing function. -/
675 theorem strict_antimono_of_deriv_neg {f : ℝ → ℝ} (hf : differentiable ℝ f)
id ┴ ┴ └────────────┘ ┴ ┴
src ┴ ┴ └────────────┘ ┴
typ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────┘
676 (hf' : ∀ x, deriv f x < 0) :
id ┴ └───┘ ┴ ┴ ┴
src └───┘ ┴
typ ┴ └───┘ ┴ ┴ ┴
doc └───┘
677 ∀ ⦃x y⦄, x < y → f y < f x :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
678 λ x y hxy, convex_univ.strict_antimono_of_deriv_neg hf.continuous.continuous_on hf.differentiable_on
id ┴ ┴ └─┘ └─────────┘└───────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
src └─────────┘└───────────────────────────┘ └─────────┘└────────────┘ └────────────────┘
typ ┴ ┴ └─┘ └─────────┘└───────────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
doc └───────────────────────────┘
679 (λ x _, hf' x) x y trivial trivial hxy
id ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ └─────┘ └─┘
src └─────┘ └─────┘
typ ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ └─────┘ └─┘
680
681 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
682 of the real line. If `f` is differentiable on the interior of `D` and `f'` is nonpositive, then
683 `f` is a monotonically decreasing function on `D`. -/
684 theorem convex.antimono_of_deriv_nonpos {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id └─┘ ┴ └────┘ ┴ ┴ ┴
src └─┘ ┴ └────┘ ┴ ┴
typ └─┘ ┴ └────┘ ┴ ┴ ┴
doc └────┘
685 (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
src └───────────┘ └───────────────┘ ┴ └──────┘
typ └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
doc └───────────┘ └───────────────┘ └──────┘
686 (hf'_nonpos : ∀ x ∈ interior D, deriv f x ≤ 0) :
id ┴ └──────┘ ┴ └───┘ ┴ ┴ ┴
src └──────┘ └───┘ ┴
typ ┴ └──────┘ ┴ └───┘ ┴ ┴ ┴
doc └──────┘ └───┘
687 ∀ x y ∈ D, x ≤ y → f y ≤ f x :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
688 by simpa only [zero_mul, sub_nonpos] using hD.image_sub_le_mul_sub_of_deriv_le hf hf' hf'_nonpos
id └──────┘ └────────┘ └─────────────────────────────────┘ └┘ └─┘ └────────┘
src └──────────┘└──────┘└┘└────────┘└──────┘└─────────────────────────────────┘┴ ┴ ┴ └
typ └──────────┘└──────┘└┘└────────┘└──────┘└─────────────────────────────────┘┴└┘┴└─┘┴└────────┘└
doc └──────────┘ └┘ └──────┘└─────────────────────────────────┘┴ ┴ ┴ └
txt └──────────┘ └┘ └──────┘ ┴ ┴ ┴ └
par └──────────┘ └┘ └──────┘ ┴ ┴ ┴ └
pid ┴└──┘└┘ └┘ ┴┴└────┘ ┴ ┴ ┴ └
st └──────────────────────────────────────────────────────────────────────────────────────────────
689
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
690 /-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is nonpositive, then
691 `f` is a monotonically decreasing function. -/
692 theorem antimono_of_deriv_nonpos {f : ℝ → ℝ} (hf : differentiable ℝ f) (hf' : ∀ x, deriv f x ≤ 0) :
id ┴ ┴ └────────────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
src ┴ ┴ └────────────┘ ┴ └───┘ ┴
typ ┴ ┴ └────────────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴
doc └────────────┘ └───┘
693 ∀ ⦃x y⦄, x ≤ y → f y ≤ f x :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
694 λ x y hxy, convex_univ.antimono_of_deriv_nonpos hf.continuous.continuous_on hf.differentiable_on
id ┴ ┴ └─┘ └─────────┘└───────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
src └─────────┘└───────────────────────┘ └─────────┘└────────────┘ └────────────────┘
typ ┴ ┴ └─┘ └─────────┘└───────────────────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
doc └───────────────────────┘
695 (λ x _, hf' x) x y trivial trivial hxy
id ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ └─────┘ └─┘
src └─────┘ └─────┘
typ ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ └─────┘ └─┘
696
697 /-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is differentiable on its interior,
698 and `f'` is monotone on the interior, then `f` is convex on `D`. -/
699 theorem convex_on_of_deriv_mono {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id └─┘ ┴ └────┘ ┴ ┴ ┴
src └─┘ ┴ └────┘ ┴ ┴
typ └─┘ ┴ └────┘ ┴ ┴ ┴
doc └────┘
700 (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
src └───────────┘ └───────────────┘ ┴ └──────┘
typ └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
doc └───────────┘ └───────────────┘ └──────┘
701 (hf'_mono : ∀ x y ∈ interior D, x ≤ y → deriv f x ≤ deriv f y) :
id ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └──────┘ ┴ └───┘ ┴ └───┘
typ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
doc └──────┘ └───┘ └───┘
702 convex_on D f :=
id └───────┘ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴
doc └───────┘
703 convex_on_real_of_slope_mono_adjacent hD
id └───────────────────────────────────┘ └┘
src └───────────────────────────────────┘
typ └───────────────────────────────────┘ └┘
doc └───────────────────────────────────┘
704 begin
st └─────
705 intros x y z hx hz hxy hyz,
src └────────────────────────┘
typ └────────────────────────┘
doc └────────────────────────┘
txt └────────────────────────┘
par └────────────────────────┘
pid └──────────────────┘
st ───────────────────────────┘└─
706 -- First we prove some trivial inclusions
st ────────────────────────────────────────────
707 have hxzD : Icc x z ⊆ D, from convex_real_iff.1 hD hx hz,
id └─┘ ┴ ┴ ┴ ┴ └─────────────┘ └┘ └┘ └┘
src └──────────┘└─┘┴ ┴ ┴┴┴ └───┘└─────────────┘└─┘ ┴ ┴
typ └──────────┘└─┘┴┴┴┴┴┴┴┴ └───┘└─────────────┘└─┘└┘┴└┘┴└┘
doc └──────────┘└─┘┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴
txt └──────────┘ ┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴
par └──────────┘ ┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴
pid └───────┘└─┘ ┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴
st ────────────────────────┘└───────────────────────────────┘└─
708 have hxyD : Icc x y ⊆ D, from subset.trans (Icc_subset_Icc_right $ le_of_lt hyz) hxzD,
id └─┘ ┴ ┴ ┴ └──────────┘ └──────────────────┘ └──────┘ └─┘ └──┘
src └──────────┘└─┘┴ ┴ ┴ ┴ └───┘└──────────┘┴ └──────────────────┘┴ ┴└──────┘┴ └┘
typ └──────────┘└─┘┴┴┴┴┴ ┴┴ └───┘└──────────┘┴ └──────────────────┘┴ ┴└──────┘┴└─┘└┘└──┘
doc └──────────┘└─┘┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └┘
txt └──────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └┘
par └──────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └┘
pid └───────┘└─┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └┘
st ────────────────────────┘└────────────────────────────────────────────────────────────┘└─
709 have hxyD' : Ioo x y ⊆ interior D,
id └─┘ ┴ ┴ └──────┘ ┴
src └───────────┘└─┘┴ ┴ ┴ ┴└──────┘┴
typ └───────────┘└─┘┴┴┴┴┴ ┴└──────┘┴┴
doc └───────────┘└─┘┴ ┴ ┴ ┴└──────┘┴
txt └───────────┘ ┴ ┴ ┴ ┴ ┴
par └───────────┘ ┴ ┴ ┴ ┴ ┴
pid └────────┘└─┘ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────┘└─
710 from subset_sUnion_of_mem ⟨is_open_Ioo, subset.trans Ioo_subset_Icc_self hxyD⟩,
id └──────────────────┘ └─────────┘ └──────────┘ └─────────────────┘ └──┘
src └───┘└──────────────────┘┴ └─────────┘└┘└──────────┘┴└─────────────────┘┴ ┴
typ └───┘└──────────────────┘┴ └─────────┘└┘└──────────┘┴└─────────────────┘┴└──┘┴
doc └───┘ ┴ └┘ ┴ ┴ ┴
txt └───┘ ┴ └┘ ┴ ┴ ┴
par └───┘ ┴ └┘ ┴ ┴ ┴
pid └───┘ ┴ └┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────────┘└─
711 have hyzD : Icc y z ⊆ D, from subset.trans (Icc_subset_Icc_left $ le_of_lt hxy) hxzD,
id └─┘ ┴ ┴ ┴ └──────────┘ └─────────────────┘ └──────┘ └─┘ └──┘
src └──────────┘└─┘┴ ┴ ┴ ┴ └───┘└──────────┘┴ └─────────────────┘┴ ┴└──────┘┴ └┘
typ └──────────┘└─┘┴┴┴┴┴ ┴┴ └───┘└──────────┘┴ └─────────────────┘┴ ┴└──────┘┴└─┘└┘└──┘
doc └──────────┘└─┘┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └┘
txt └──────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └┘
par └──────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └┘
pid └───────┘└─┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └┘
st ────────────────────────┘└───────────────────────────────────────────────────────────┘└─
712 have hyzD' : Ioo y z ⊆ interior D,
id └─┘ ┴ ┴ └──────┘ ┴
src └───────────┘└─┘┴ ┴ ┴ ┴└──────┘┴
typ └───────────┘└─┘┴┴┴┴┴ ┴└──────┘┴┴
doc └───────────┘└─┘┴ ┴ ┴ ┴└──────┘┴
txt └───────────┘ ┴ ┴ ┴ ┴ ┴
par └───────────┘ ┴ ┴ ┴ ┴ ┴
pid └────────┘└─┘ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────┘└─
713 from subset_sUnion_of_mem ⟨is_open_Ioo, subset.trans Ioo_subset_Icc_self hyzD⟩,
id └──────────────────┘ └─────────┘ └──────────┘ └─────────────────┘ └──┘
src └───┘└──────────────────┘┴ └─────────┘└┘└──────────┘┴└─────────────────┘┴ ┴
typ └───┘└──────────────────┘┴ └─────────┘└┘└──────────┘┴└─────────────────┘┴└──┘┴
doc └───┘ ┴ └┘ ┴ ┴ ┴
txt └───┘ ┴ └┘ ┴ ┴ ┴
par └───┘ ┴ └┘ ┴ ┴ ┴
pid └───┘ ┴ └┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────────┘└─
714 -- Then we apply MVT to both `[x, y]` and `[y, z]`
st ─────────────────────────────────────────────────────
715 obtain ⟨a, ⟨hxa, hay⟩, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x),
id ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────────────────────┘┴└───┘└─┘┴ ┴ ┴┴└───┘┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ └┘┴┴ ┴ ┴ ┴
typ └───────────────────────────┘┴└───┘└─┘┴ ┴ ┴┴└───┘┴ ┴ ┴┴┴ ┴ ┴┴┴┴┴ └┘┴┴ ┴┴ ┴┴┴
doc └───────────────────────────┘ └───┘└─┘┴ ┴ ┴└───┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
txt └───────────────────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
par └───────────────────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
pid └─────────────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────┘└─
716 from exists_deriv_eq_slope f hxy (hf.mono hxyD) (hf'.mono hxyD'),
id └───────────────────┘ ┴ └─┘ └─────┘ └──┘ └──────┘ └───┘
src └───┘└───────────────────┘┴ ┴ ┴ └─────┘┴ └┘ └──────┘┴ ┴
typ └───┘└───────────────────┘┴┴┴└─┘┴ └─────┘┴└──┘└┘ └──────┘┴└───┘┴
doc └───┘└───────────────────┘┴ ┴ ┴ ┴ └┘ ┴ ┴
txt └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
par └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
pid └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
st ───────────────────────────────────────────────────────────────────┘└─
717 obtain ⟨b, ⟨hyb, hbz⟩, hb⟩ : ∃ b ∈ Ioo y z, deriv f b = (f z - f y) / (z - y),
id ┴ └─┘ ┴ └───┘ ┴ ┴ ┴
src └───────────────────────────┘┴└───┘└─┘┴ ┴ ┴┴└───┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
typ └───────────────────────────┘┴└───┘└─┘┴ ┴ ┴┴└───┘┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ └┘ ┴ ┴┴ ┴┴┴
doc └───────────────────────────┘ └───┘└─┘┴ ┴ ┴└───┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
txt └───────────────────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
par └───────────────────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
pid └─────────────────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────┘└─
718 from exists_deriv_eq_slope f hyz (hf.mono hyzD) (hf'.mono hyzD'),
id └───────────────────┘ ┴ └─┘ └─────┘ └──┘ └──────┘ └───┘
src └───┘└───────────────────┘┴ ┴ ┴ └─────┘┴ └┘ └──────┘┴ ┴
typ └───┘└───────────────────┘┴┴┴└─┘┴ └─────┘┴└──┘└┘ └──────┘┴└───┘┴
doc └───┘└───────────────────┘┴ ┴ ┴ ┴ └┘ ┴ ┴
txt └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
par └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
pid └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
st ───────────────────────────────────────────────────────────────────┘└─
719 rw [← ha, ← hb],
id └┘ └┘
src └────┘ └──┘ ┴
typ └────┘└┘└──┘└┘┴
doc └────┘ └──┘ ┴
txt └────┘ └──┘ ┴
par └────┘ └──┘ ┴
pid └──┘ └──┘ ┴
st ─────────┘└────┘└──
720 exact hf'_mono a b (hxyD' ⟨hxa, hay⟩) (hyzD' ⟨hyb, hbz⟩) (le_of_lt $ lt_trans hay hyb)
id └──────┘ ┴ ┴ └───┘ └─┘ └───┘ └─┘ └──────┘ └──────┘ └─┘ └─┘
src └────┘ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ └┘ └─┘ └──────┘┴ ┴└──────┘┴ ┴ └┘
typ └────┘└──────┘┴┴┴┴┴ └───┘┴ └─┘└┘ └─┘ └───┘┴ └┘└─┘└─┘ └──────┘┴ ┴└──────┘┴└─┘┴└─┘└┘
doc └────┘ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ └┘ └─┘ ┴ ┴ ┴ ┴ ┴┴
st ────────────────────────────────────────────────────────────────────────────────────────┘
721 end
st └─┘
722
723 /-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is differentiable on its interior,
724 and `f'` is monotone on the interior, then `f` is convex on `ℝ`. -/
725 theorem convex_on_univ_of_deriv_mono {f : ℝ → ℝ} (hf : differentiable ℝ f)
id ┴ ┴ └────────────┘ ┴ ┴
src ┴ ┴ └────────────┘ ┴
typ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────┘
726 (hf'_mono : monotone (deriv f)) : convex_on univ f :=
id └──────┘ └───┘ ┴ └───────┘ └──┘ ┴
src └──────┘ └───┘ └───────┘ └──┘
typ └──────┘ └───┘ ┴ └───────┘ └──┘ ┴
doc └──────┘ └───┘ └───────┘
727 convex_on_of_deriv_mono convex_univ hf.continuous.continuous_on hf.differentiable_on
id └─────────────────────┘ └─────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
src └─────────────────────┘ └─────────┘ └─────────┘└────────────┘ └────────────────┘
typ └─────────────────────┘ └─────────┘ └┘└─────────┘└────────────┘ └┘└────────────────┘
doc └─────────────────────┘
728 (λ x y _ _ h, hf'_mono h)
id ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
729
730 /-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is twice differentiable on its interior,
731 and `f''` is nonnegative on the interior, then `f` is convex on `D`. -/
732 theorem convex_on_of_deriv2_nonneg {D : set ℝ} (hD : convex D) {f : ℝ → ℝ}
id └─┘ ┴ └────┘ ┴ ┴ ┴
src └─┘ ┴ └────┘ ┴ ┴
typ └─┘ ┴ └────┘ ┴ ┴ ┴
doc └────┘
733 (hf : continuous_on f D) (hf' : differentiable_on ℝ f (interior D))
id └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
src └───────────┘ └───────────────┘ ┴ └──────┘
typ └───────────┘ ┴ ┴ └───────────────┘ ┴ ┴ └──────┘ ┴
doc └───────────┘ └───────────────┘ └──────┘
734 (hf'' : differentiable_on ℝ (deriv f) (interior D))
id └───────────────┘ ┴ └───┘ ┴ └──────┘ ┴
src └───────────────┘ ┴ └───┘ └──────┘
typ └───────────────┘ ┴ └───┘ ┴ └──────┘ ┴
doc └───────────────┘ └───┘ └──────┘
735 (hf''_nonneg : ∀ x ∈ interior D, 0 ≤ (deriv^[2] f x)) :
id ┴ └──────┘ ┴ ┴ └───┘└┘ ┴ ┴ ┴
src └──────┘ ┴ └───┘└┘ ┴
typ ┴ └──────┘ ┴ ┴ └───┘└┘ ┴ ┴ ┴
doc └──────┘ └───┘
736 convex_on D f :=
id └───────┘ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴
doc └───────┘
737 convex_on_of_deriv_mono hD hf hf' $
id └─────────────────────┘ └┘ └┘ └─┘
src └─────────────────────┘
typ └─────────────────────┘ └┘ └┘ └─┘
doc └─────────────────────┘
738 assume x y hx hy hxy,
id ┴ ┴ └┘ └┘ └─┘
typ ┴ ┴ └┘ └┘ └─┘
739 hD.interior.mono_of_deriv_nonneg hf''.continuous_on (by rwa [interior_interior])
id └┘└───────┘└───────────────────┘ └──┘└────────────┘ └───────────────┘
src └───────┘└───────────────────┘ └────────────┘ └───┘└───────────────┘┴
typ └┘└───────┘└───────────────────┘ └──┘└────────────┘ └───┘└───────────────┘┴
doc └───────┘└───────────────────┘ └───┘ ┴
txt └───┘ ┴
par └───┘ ┴
pid └┘ ┴
st └─────────────────────┘┴
740 (by rwa [interior_interior]) _ _ hx hy hxy
id └───────────────┘ └┘ └┘ └─┘
src └───┘└───────────────┘┴
typ └───┘└───────────────┘┴ └┘ └┘ └─┘
doc └───┘ ┴
txt └───┘ ┴
par └───┘ ┴
pid └┘ ┴
st └─────────────────────┘┴
741
742 /-- If a function `f` is twice differentiable on `ℝ`, and `f''` is nonnegative on `ℝ`,
743 then `f` is convex on `ℝ`. -/
744 theorem convex_on_univ_of_deriv2_nonneg {f : ℝ → ℝ} (hf' : differentiable ℝ f)
id ┴ ┴ └────────────┘ ┴ ┴
src ┴ ┴ └────────────┘ ┴
typ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────┘
745 (hf'' : differentiable ℝ (deriv f)) (hf''_nonneg : ∀ x, 0 ≤ (deriv^[2] f x)) :
id └────────────┘ ┴ └───┘ ┴ ┴ ┴ └───┘└┘ ┴ ┴ ┴
src └────────────┘ ┴ └───┘ ┴ └───┘└┘ ┴
typ └────────────┘ ┴ └───┘ ┴ ┴ ┴ └───┘└┘ ┴ ┴ ┴
doc └────────────┘ └───┘ └───┘
746 convex_on univ f :=
id └───────┘ └──┘ ┴
src └───────┘ └──┘
typ └───────┘ └──┘ ┴
doc └───────┘
747 convex_on_of_deriv2_nonneg convex_univ hf'.continuous.continuous_on hf'.differentiable_on
id └────────────────────────┘ └─────────┘ └─┘└─────────┘└────────────┘ └─┘└────────────────┘
src └────────────────────────┘ └─────────┘ └─────────┘└────────────┘ └────────────────┘
typ └────────────────────────┘ └─────────┘ └─┘└─────────┘└────────────┘ └─┘└────────────────┘
doc └────────────────────────┘
748 hf''.differentiable_on (λ x _, hf''_nonneg x)
id └──┘└────────────────┘ ┴ ┴ └─────────┘ ┴
src └────────────────┘
typ └──┘└────────────────┘ ┴ ┴ └─────────┘ ┴